1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Gluing metric spaces
  5  Authors: Sébastien Gouëzel
  6  -/
  7  
  8  import topology.metric_space.isometry topology.metric_space.premetric_space
src         └────────────────────────────┘ └───────────────────────────────────┘
  9  
 10  /-!
 11  # Metric space gluing
 12  
 13  Gluing two metric spaces along a common subset. Formally, we are given
 14  
 15  ```
 16       Φ
 17    γ ---> α
 18    |
 19    |Ψ
 20    v
 21    β
 22  ```
 23  where `hΦ : isometry Φ` and `hΨ : isometry Ψ`.
 24  We want to complete the square by a space `glue_space hΦ hΨ` and two isometries
 25  `to_glue_l hΦ hΨ` and `to_glue_r hΦ hΨ` that make the square commute.
 26  We start by defining a predistance on the disjoint union `α ⊕ β`, for which
 27  points `Φ p` and `Ψ p` are at distance 0. The (quotient) metric space associated
 28  to this predistance is the desired space.
 29  
 30  This is an instance of a more general construction, where `Φ` and `Ψ` do not have to be isometries,
 31  but the distances in the image almost coincide, up to `2ε` say. Then one can almost glue the two
 32  spaces so that the images of a point under `Φ` and `Ψ` are ε-close. If `ε > 0`, this yields a
 33  metric space structure on `α ⊕ β`, without the need to take a quotient. In particular, when
 34  `α` and `β` are inhabited, this gives a natural metric space structure on `α ⊕ β`, where the basepoints
 35  are at distance 1, say, and the distances between other points are obtained by going through the
 36  two basepoints.
 37  
 38  We also define the inductive limit of metric spaces. Given
 39  ```
 40       f 0        f 1        f 2        f 3
 41  X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...
 42  ```
 43  where the `X n` are metric spaces and `f n` isometric embeddings, we define the inductive
 44  limit of the `X n`, also known as the increasing union of the `X n` in this context, if we
 45  identify `X n` and `X (n+1)` through `f n`. This is a metric space in which all `X n` embed
 46  isometrically and in a way compatible with `f n`.
 47  
 48  -/
 49  
 50  noncomputable theory
 51  
 52  universes u v w
 53  variables {α : Type u} {β : Type v} {γ : Type w}
 54  
 55  open function set premetric lattice
 56  
 57  namespace metric
 58  section approx_gluing
 59  
 60  variables [metric_space α] [metric_space β]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
doc             └──────────┘     └──────────┘
 61            {Φ : γ → α} {Ψ : γ → β} {ε : ℝ}
id                                          
src                                         
typ                                         
 62  open lattice
 63  open sum (inl inr)
 64  
 65  /-- Define a predistance on α ⊕ β, for which Φ p and Ψ p are at distance ε -/
 66  def glue_dist (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) : α ⊕ β → α ⊕ β → ℝ
id                                                       
src                                                               
typ                                                      
 67  | (inl x) (inl y) := dist x y
id             └─┘      └──┘
src             └─┘       └──┘
typ            └─┘      └──┘
 68  | (inr x) (inr y) := dist x y
id             └─┘      └──┘
src             └─┘       └──┘
typ            └─┘      └──┘
 69  | (inl x) (inr y) := infi (λp, dist x (Φ p) + dist y (Ψ p)) + ε
id      └─┘    └─┘      └──┘     └──┘        └──┘         
src     └─┘     └─┘       └──┘      └──┘          └──┘          
typ     └─┘    └─┘      └──┘     └──┘        └──┘         
doc                       └──┘
 70  | (inr x) (inl y) := infi (λp, dist y (Φ p) + dist x (Ψ p)) + ε
id      └─┘    └─┘      └──┘     └──┘        └──┘         
src     └─┘     └─┘       └──┘      └──┘          └──┘          
typ     └─┘    └─┘      └──┘     └──┘        └──┘         
doc                       └──┘
 71  
 72  private lemma glue_dist_self (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) : ∀x, glue_dist Φ Ψ ε x x = 0
id                                                                └───────┘      
src                                                                    └───────┘           
typ                                                               └───────┘      
doc                                                                     └───────┘
 73  | (inl x) := dist_self _
id      └─┘       └───────┘
src     └─┘       └───────┘
typ     └─┘       └───────┘
 74  | (inr x) := dist_self _
id      └─┘       └───────┘
src     └─┘       └───────┘
typ     └─┘       └───────┘
 75  
 76  lemma glue_dist_glued_points [nonempty γ] (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (p : γ) :
id                                 └──────┘                                   
src                                └──────┘                                 
typ                                └──────┘                                   
 77    glue_dist Φ Ψ ε (inl (Φ p)) (inr (Ψ p)) = ε :=
id     └───────┘     └─┘       └─┘       
src    └───────┘        └─┘         └─┘        
typ    └───────┘     └─┘       └─┘       
doc    └───────┘
 78  begin
 79    have : infi (λq, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0,
id            └──┘                       └──┘            
src    └─────┘└──┘  └─┘       └┘   └┘└──┘   └┘   └─┘└┘
typ    └─────┘└──┘  └─┘       └┘  └┘└──┘  └┘  └─┘└┘
doc    └─────┘└──┘  └─┘       └┘   └┘        └┘   └─┘ └┘
txt    └─────┘      └─┘       └┘   └┘        └┘   └─┘ └┘
par    └─────┘      └─┘       └┘   └┘        └┘   └─┘ └┘
pid    └───┘└┘      └─┘       └┘   └┘        └┘   └─┘ 
st            └────────────────────────────────────────────────┘└─
 80    { have A : ∀q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) :=
id                                         └──┘       
src      └───────┘  └─┘       └┘   └┘ └──┘   └┘   └────
typ      └───────┘  └─┘       └┘  └┘ └──┘  └┘  └────
doc      └───────┘  └─┘        └┘   └┘        └┘   └────
txt      └───────┘  └─┘        └┘   └┘        └┘   └────
par      └───────┘  └─┘        └┘   └┘        └┘   └────
pid      └────┘└─┘  └─┘        └┘   └┘        └┘   └───
st   ───┘└───────────────────────────────────────────────────────
 81        λq, by rw ← add_zero (0 : ℝ); exact add_le_add dist_nonneg dist_nonneg,
id                     └──────┘                └────────┘             └─────────┘
src  ─────┘ └─┘  └───┘└──────┘ └──┘ └┘└────┘└────────┘           └─────────┘
typ  ─────┘ └─┘  └───┘└──────┘ └──┘ └┘└────┘└────────┘           └─────────┘
doc  ─────┘ └─┘  └───┘         └──┘ └┘└────┘                     
txt  ─────┘ └─┘  └───┘         └──┘ └┘└────┘                     
par  ─────┘ └─┘  └───┘         └──┘ └┘└────┘                     
pid  ─────┘ └─┘  └────┘         └──┘ └───────┘                     
st   ───────────┘└──────────────────────────────────────────────────────────────┘└─
 82      refine le_antisymm _ (le_cinfi A),
id              └─────────┘    └──────┘ 
src      └─────┘└─────────┘└─┘ └──────┘ 
typ      └─────┘└─────────┘└─┘ └──────┘
doc      └─────┘           └─┘ └──────┘ 
txt      └─────┘           └─┘          
par      └─────┘           └─┘          
pid                       └─┘          
st   ────────────────────────────────────┘└─
 83      have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p), by simp,
id                                    └──┘         
src      └───────┘        └┘   └┘ └──┘   └┘        └──┘
typ      └───────┘        └┘  └┘ └──┘   └┘      └──┘
doc      └───────┘        └┘   └┘        └┘        └──┘
txt      └───────┘        └┘   └┘        └┘        └──┘
par      └───────┘        └┘   └┘        └┘        └──┘
pid      └───┘└──┘        └┘   └┘        └┘   
st   ─────────────────────────────────────────────────┘         └─
 84      rw this,
id          └──┘
src      └─┘
typ      └─┘└──┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
 85      exact cinfi_le ⟨0, forall_range_iff.2 A⟩ },
id             └──────┘     └──────────────┘   
src      └────┘└──────┘ └─┘└──────────────┘└─┘ └┘
typ      └────┘└──────┘ └─┘└──────────────┘└─┘└┘
doc      └────┘└──────┘ └─┘                └─┘ └┘
txt      └────┘         └─┘                └─┘ └┘
par      └────┘         └─┘                └─┘ └┘
pid                    └─┘                └─┘ 
st   ────────────────────────────────────────────┘└┘
 86    rw [glue_dist, this, zero_add]
id         └───────┘  └──┘  └──────┘
src    └──┘└───────┘└┘    └┘└──────┘└┘
typ    └──┘└───────┘└┘└──┘└┘└──────┘└┘
doc    └──┘└───────┘└┘    └┘        └┘
txt    └──┘         └┘    └┘        └┘
par    └──┘         └┘    └┘        └┘
pid      └┘         └┘    └┘        
st   ──────────────┘└────┘└────────┘
 87  end
st   └─┘
 88  
 89  private lemma glue_dist_comm (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) :
id                                                         
src                                                            
typ                                                        
 90    ∀x y, glue_dist Φ Ψ ε x y = glue_dist Φ Ψ ε y x
id         └───────┘       └───────┘     
src          └───────┘            └───────┘
typ        └───────┘       └───────┘     
doc          └───────┘             └───────┘
 91  | (inl x) (inl y) := dist_comm _ _
id              └─┘       └───────┘
src             └─┘       └───────┘
typ             └─┘       └───────┘
 92  | (inr x) (inr y) := dist_comm _ _
id              └─┘       └───────┘
src             └─┘       └───────┘
typ             └─┘       └───────┘
 93  | (inl x) (inr y) := rfl
id      └─┘     └─┘       └─┘
src     └─┘     └─┘       └─┘
typ     └─┘     └─┘       └─┘
 94  | (inr x) (inl y) := rfl
id      └─┘     └─┘       └─┘
src     └─┘     └─┘       └─┘
typ     └─┘     └─┘       └─┘
 95  
 96  variable [nonempty γ]
id             └──────┘
src            └──────┘
typ            └──────┘
 97  
 98  private lemma glue_dist_triangle (Φ : γ → α) (Ψ : γ → β) (ε : ℝ)
id                                                             
src                                                                
typ                                                            
 99    (H : ∀p q, abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε) :
id              └─┘  └──┘          └──┘              
src               └─┘  └──┘              └──┘                 
typ             └─┘  └──┘          └──┘              
100    ∀x y z, glue_dist Φ Ψ ε x z ≤ glue_dist Φ Ψ ε x y + glue_dist Φ Ψ ε y z
id          └───────┘       └───────┘       └───────┘     
src            └───────┘            └───────┘            └───────┘
typ         └───────┘       └───────┘       └───────┘     
doc            └───────┘             └───────┘             └───────┘
101  | (inl x) (inl y) (inl z) := dist_triangle _ _ _
id                      └─┘       └───────────┘
src                     └─┘       └───────────┘
typ                     └─┘       └───────────┘
102  | (inr x) (inr y) (inr z) := dist_triangle _ _ _
id                      └─┘       └───────────┘
src                     └─┘       └───────────┘
typ                     └─┘       └───────────┘
103  | (inr x) (inl y) (inl z) := begin
id      └─┘             └─┘
src     └─┘             └─┘
typ     └─┘             └─┘
st                                └─────
104      have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id                      └───────┘  └───┘                         └──┘    
src      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘└──┘    └──────
typ      └───────┘ └─┘ └───────┘ └───┘  └────┘└─┘       └┘└──┘   └──────
doc      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘         └──────
txt      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
par      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
pid      └────┘└─┘ └─┘                  └────┘ └─┘        └┘         └─┘└───
st   ─────────────────────────────────────────────────────────────────────────────────
105        λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id                   └──────────────┘        └────────┘             └─────────┘
src  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
typ  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
doc  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
txt  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
par  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
pid  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
106      unfold glue_dist,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
107      have : infi (λp, dist z (Φ p) + dist x (Ψ p)) ≤ infi (λp, dist y (Φ p) + dist x (Ψ p)) + dist y z,
id                                                      └──┘                                  └──┘  
src      └─────┘      └─┘        └┘         └─┘└──┘  └─┘        └┘         └─┘ └──┘ 
typ      └─────┘      └─┘        └┘         └─┘└──┘  └─┘       └┘       └─┘ └──┘
doc      └─────┘      └─┘        └┘         └─┘ └──┘  └─┘        └┘         └─┘      
txt      └─────┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
par      └─────┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
pid      └───┘└┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
108      { have : infi (λp, dist y (Φ p) + dist x (Ψ p)) + dist y z =
id                                                                  
src        └─────┘      └─┘        └┘         └─┘       
typ        └─────┘      └─┘        └┘         └─┘       
doc        └─────┘      └─┘        └┘         └─┘        
txt        └─────┘      └─┘        └┘         └─┘        
par        └─────┘      └─┘        └┘         └─┘        
pid        └───┘└┘      └─┘        └┘         └─┘        
st   ─────┘└──────────────────────────────────────────────────────────
109              infi ((λt, t + dist y z) ∘ (λp, dist y (Φ p) + dist x (Ψ p))),
id               └──┘                                       └──┘   
src  ───────────┘└──┘   └─┘        └┘  └─┘        └┘ └──┘    └─┘
typ  ───────────┘└──┘   └─┘       └┘  └─┘      └┘ └──┘  └─┘
doc  ───────────┘└──┘   └─┘        └┘   └─┘        └┘         └─┘
txt  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
par  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
pid  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
110        { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, t + dist y z)) _ (B _ _),
id                  └──────────────────────────────────────┘      └────────┘          └──┘        
src          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘  └──┘  └───┘  └───┘
typ          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘  └──┘└───┘ └───┘
doc          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘        └───┘  └───┘
txt          └─────┘                                         └──┘            └─┘        └───┘  └───┘
par          └─────┘                                         └──┘            └─┘        └───┘  └───┘
pid                                                         └──┘            └─┘        └───┘  └───┘
st   ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
111          exact continuous_id.add continuous_const,
id                 └───────────────┘ └──────────────┘
src          └────┘└───────────────┘└──────────────┘
typ          └────┘└───────────────┘└──────────────┘
doc          └────┘                 
txt          └────┘                 
par          └────┘                 
pid                                
st   ───────────────────────────────────────────────┘└─
112          exact λx y hx, by simpa },
src          └────┘ └──────┘  └────┘
typ          └────┘ └──────┘  └────┘
doc          └────┘ └──────┘  └────┘
txt          └────┘ └──────┘  └────┘
par          └────┘ └──────┘  └────┘
pid                └──────┘  └─────┘
st   ────────────────────────┘└─────┘└┘
113        rw [this, comp],
id             └──┘  └──┘
src        └──┘    └┘└──┘
typ        └──┘└──┘└┘└──┘
doc        └──┘    └┘    
txt        └──┘    └┘    
par        └──┘    └┘    
pid          └┘    └┘    
st   ─────────────┘└────┘└──
114        refine cinfi_le_cinfi (B _ _) (λp, _),
id                └────────────┘  
src        └─────┘└────────────┘  └────┘  └───┘
typ        └─────┘└────────────┘ └────┘  └───┘
doc        └─────┘└────────────┘  └────┘  └───┘
txt        └─────┘                └────┘  └───┘
par        └─────┘                └────┘  └───┘
pid                              └────┘  └───┘
st   ──────────────────────────────────────────┘└─
115        calc
id         └──┘
src        └──┘
typ        └──┘
doc        └──┘
st   ───────────
116          dist z (Φ p) + dist x (Ψ p) ≤ (dist y z + dist y (Φ p)) + dist x (Ψ p) :
st   ─────────────────────────────────────────────────────────────────────────────────
117            add_le_add (dist_triangle_left _ _ _) (le_refl _)
id             └────────┘  └────────────────┘         └─────┘
src            └────────┘  └────────────────┘         └─────┘
typ            └────────┘  └────────────────┘         └─────┘
st   ────────────────────────────────────────────────────────────
118          ... = dist y (Φ p) + dist x (Ψ p) + dist y z : by ring },
id                                           └──┘  
src                                              └──┘          └───┘
typ                                          └──┘        └───┘
doc                                                            └───┘
txt                                                            └───┘
par                                                            └───┘
pid                                                                
st   ────────────────────────────────────────────────────────┘└────┘└┘
119      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
120    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
121  | (inr x) (inr y) (inl z) := begin
id              └─┘     └─┘
src             └─┘     └─┘
typ             └─┘     └─┘
st                                └─────
122      have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id                      └───────┘  └───┘                          └──┘    
src      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘ └──┘    └──────
typ      └───────┘ └─┘ └───────┘ └───┘  └────┘└─┘       └┘ └──┘   └──────
doc      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘         └──────
txt      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
par      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
pid      └────┘└─┘ └─┘                  └────┘ └─┘        └┘         └─┘└───
st   ─────────────────────────────────────────────────────────────────────────────────
123        λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id                   └──────────────┘        └────────┘             └─────────┘
src  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
typ  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
doc  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
txt  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
par  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
pid  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
124      unfold glue_dist,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
125      have : infi (λp, dist z (Φ p) + dist x (Ψ p)) ≤ dist x y + infi (λp, dist z (Φ p) + dist y (Ψ p)),
id                                                                 └──┘                   └──┘   
src      └─────┘      └─┘        └┘         └─┘        └──┘  └─┘        └┘ └──┘    └┘
typ      └─────┘      └─┘        └┘         └─┘       └──┘  └─┘      └┘ └──┘  └┘
doc      └─────┘      └─┘        └┘         └─┘        └──┘  └─┘        └┘         └┘
txt      └─────┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
par      └─────┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
pid      └───┘└┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
126      { have : dist x y + infi (λp, dist z (Φ p) + dist y (Ψ p)) =
src        └─────┘             └─┘        └┘         └─┘ 
typ        └─────┘             └─┘        └┘         └─┘ 
doc        └─────┘             └─┘        └┘         └─┘ 
txt        └─────┘             └─┘        └┘         └─┘ 
par        └─────┘             └─┘        └┘         └─┘ 
pid        └───┘└┘             └─┘        └┘         └─┘ 
st   ─────┘└──────────────────────────────────────────────────────────
127              infi ((λt, dist x y + t) ∘ (λp, dist z (Φ p) + dist y (Ψ p))),
id               └──┘                                        └──┘   
src  ───────────┘└──┘   └─┘        └┘   └─┘        └┘ └──┘    └─┘
typ  ───────────┘└──┘   └─┘       └┘   └─┘      └┘ └──┘  └─┘
doc  ───────────┘└──┘   └─┘        └┘   └─┘        └┘         └─┘
txt  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
par  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
pid  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
128        { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, dist x y + t)) _ (B _ _),
id                  └──────────────────────────────────────┘      └────────┘      └──┘            
src          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘└──┘    └───┘  └───┘
typ          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘└──┘  └───┘ └───┘
doc          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘        └───┘  └───┘
txt          └─────┘                                         └──┘            └─┘        └───┘  └───┘
par          └─────┘                                         └──┘            └─┘        └───┘  └───┘
pid                                                         └──┘            └─┘        └───┘  └───┘
st   ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
129          exact continuous_const.add continuous_id,
id                 └──────────────────┘ └───────────┘
src          └────┘└──────────────────┘└───────────┘
typ          └────┘└──────────────────┘└───────────┘
doc          └────┘                    
txt          └────┘                    
par          └────┘                    
pid                                   
st   ───────────────────────────────────────────────┘└─
130          exact λx y hx, by simpa },
src          └────┘ └──────┘  └────┘
typ          └────┘ └──────┘  └────┘
doc          └────┘ └──────┘  └────┘
txt          └────┘ └──────┘  └────┘
par          └────┘ └──────┘  └────┘
pid                └──────┘  └─────┘
st   ────────────────────────┘└─────┘└┘
131        rw [this, comp],
id             └──┘  └──┘
src        └──┘    └┘└──┘
typ        └──┘└──┘└┘└──┘
doc        └──┘    └┘    
txt        └──┘    └┘    
par        └──┘    └┘    
pid          └┘    └┘    
st   ─────────────┘└────┘└──
132        refine cinfi_le_cinfi (B _ _) (λp, _),
id                └────────────┘  
src        └─────┘└────────────┘  └────┘  └───┘
typ        └─────┘└────────────┘ └────┘  └───┘
doc        └─────┘└────────────┘  └────┘  └───┘
txt        └─────┘                └────┘  └───┘
par        └─────┘                └────┘  └───┘
pid                              └────┘  └───┘
st   ──────────────────────────────────────────┘└─
133        calc
id         └──┘
src        └──┘
typ        └──┘
doc        └──┘
st   ───────────
134          dist z (Φ p) + dist x (Ψ p) ≤ dist z (Φ p) + (dist x y + dist y (Ψ p)) :
st   ─────────────────────────────────────────────────────────────────────────────────
135            add_le_add (le_refl _) (dist_triangle _ _ _)
id             └────────┘  └─────┘     └───────────┘
src            └────────┘  └─────┘     └───────────┘
typ            └────────┘  └─────┘     └───────────┘
st   ───────────────────────────────────────────────────────
136          ... = dist x y + (dist z (Φ p) + dist y (Ψ p)) : by ring },
id                                         └──┘    
src                                           └──┘               └───┘
typ                                        └──┘            └───┘
doc                                                              └───┘
txt                                                              └───┘
par                                                              └───┘
pid                                                                  
st   ──────────────────────────────────────────────────────────┘└────┘└┘
137      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
138    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
139  | (inl x) (inl y) (inr z) := begin
id              └─┘     └─┘
src             └─┘     └─┘
typ             └─┘     └─┘
st                                └─────
140      have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id                      └───────┘  └───┘                          └──┘    
src      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘ └──┘    └──────
typ      └───────┘ └─┘ └───────┘ └───┘  └────┘└─┘       └┘ └──┘   └──────
doc      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘         └──────
txt      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
par      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
pid      └────┘└─┘ └─┘                  └────┘ └─┘        └┘         └─┘└───
st   ─────────────────────────────────────────────────────────────────────────────────
141        λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id                   └──────────────┘        └────────┘             └─────────┘
src  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
typ  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
doc  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
txt  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
par  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
pid  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
142      unfold glue_dist,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
143      have : infi (λp, dist x (Φ p) + dist z (Ψ p)) ≤ dist x y + infi (λp, dist y (Φ p) + dist z (Ψ p)),
id                                                                 └──┘                   └──┘   
src      └─────┘      └─┘        └┘         └─┘        └──┘  └─┘        └┘ └──┘    └┘
typ      └─────┘      └─┘        └┘         └─┘       └──┘  └─┘      └┘ └──┘  └┘
doc      └─────┘      └─┘        └┘         └─┘        └──┘  └─┘        └┘         └┘
txt      └─────┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
par      └─────┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
pid      └───┘└┘      └─┘        └┘         └─┘              └─┘        └┘         └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
144      { have : dist x y + infi (λp, dist y (Φ p) + dist z (Ψ p)) =
src        └─────┘             └─┘        └┘         └─┘ 
typ        └─────┘             └─┘        └┘         └─┘ 
doc        └─────┘             └─┘        └┘         └─┘ 
txt        └─────┘             └─┘        └┘         └─┘ 
par        └─────┘             └─┘        └┘         └─┘ 
pid        └───┘└┘             └─┘        └┘         └─┘ 
st   ─────┘└──────────────────────────────────────────────────────────
145              infi ((λt, dist x y + t) ∘ (λp, dist y (Φ p) + dist z (Ψ p))),
id               └──┘                                        └──┘   
src  ───────────┘└──┘   └─┘        └┘   └─┘        └┘ └──┘    └─┘
typ  ───────────┘└──┘   └─┘       └┘   └─┘      └┘ └──┘  └─┘
doc  ───────────┘└──┘   └─┘        └┘   └─┘        └┘         └─┘
txt  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
par  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
pid  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
146        { refine cinfi_of_cinfi_of_monotone_of_continuous ( _ : continuous (λt, dist x y + t)) _ (B _ _),
id                  └──────────────────────────────────────┘       └────────┘      └──┘            
src          └─────┘└──────────────────────────────────────┘ └───┘└────────┘  └─┘└──┘    └───┘  └───┘
typ          └─────┘└──────────────────────────────────────┘ └───┘└────────┘  └─┘└──┘  └───┘ └───┘
doc          └─────┘└──────────────────────────────────────┘ └───┘└────────┘  └─┘        └───┘  └───┘
txt          └─────┘                                         └───┘            └─┘        └───┘  └───┘
par          └─────┘                                         └───┘            └─┘        └───┘  └───┘
pid                                                         └───┘            └─┘        └───┘  └───┘
st   ───────┘└────────────────────────────────────────────────────────────────────────────────────────────┘└─
147          exact continuous_const.add continuous_id,
id                 └──────────────────┘ └───────────┘
src          └────┘└──────────────────┘└───────────┘
typ          └────┘└──────────────────┘└───────────┘
doc          └────┘                    
txt          └────┘                    
par          └────┘                    
pid                                   
st   ───────────────────────────────────────────────┘└─
148          exact λx y hx, by simpa },
src          └────┘ └──────┘  └────┘
typ          └────┘ └──────┘  └────┘
doc          └────┘ └──────┘  └────┘
txt          └────┘ └──────┘  └────┘
par          └────┘ └──────┘  └────┘
pid                └──────┘  └─────┘
st   ────────────────────────┘└─────┘└┘
149        rw [this, comp],
id             └──┘  └──┘
src        └──┘    └┘└──┘
typ        └──┘└──┘└┘└──┘
doc        └──┘    └┘    
txt        └──┘    └┘    
par        └──┘    └┘    
pid          └┘    └┘    
st   ─────────────┘└────┘└──
150        refine cinfi_le_cinfi (B _ _) (λp, _),
id                └────────────┘  
src        └─────┘└────────────┘  └────┘  └───┘
typ        └─────┘└────────────┘ └────┘  └───┘
doc        └─────┘└────────────┘  └────┘  └───┘
txt        └─────┘                └────┘  └───┘
par        └─────┘                └────┘  └───┘
pid                              └────┘  └───┘
st   ──────────────────────────────────────────┘└─
151        calc
id         └──┘
src        └──┘
typ        └──┘
doc        └──┘
st   ───────────
152          dist x (Φ p) + dist z (Ψ p) ≤ (dist x y + dist y (Φ p)) + dist z (Ψ p) :
st   ─────────────────────────────────────────────────────────────────────────────────
153            add_le_add (dist_triangle _ _ _) (le_refl _)
id             └────────┘  └───────────┘         └─────┘
src            └────────┘  └───────────┘         └─────┘
typ            └────────┘  └───────────┘         └─────┘
st   ───────────────────────────────────────────────────────
154          ... = dist x y + (dist y (Φ p) + dist z (Ψ p)) : by ring },
id                                         └──┘    
src                                           └──┘               └───┘
typ                                        └──┘            └───┘
doc                                                              └───┘
txt                                                              └───┘
par                                                              └───┘
pid                                                                  
st   ──────────────────────────────────────────────────────────┘└────┘└┘
155      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
156    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
157  | (inl x) (inr y) (inr z) := begin
id      └─┘             └─┘
src     └─┘             └─┘
typ     └─┘             └─┘
st                                └─────
158      have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id                      └───────┘  └───┘                          └──┘    
src      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘ └──┘    └──────
typ      └───────┘ └─┘ └───────┘ └───┘  └────┘└─┘       └┘ └──┘   └──────
doc      └───────┘ └─┘ └───────┘ └───┘  └────┘ └─┘        └┘         └──────
txt      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
par      └───────┘ └─┘                  └────┘ └─┘        └┘         └──────
pid      └────┘└─┘ └─┘                  └────┘ └─┘        └┘         └─┘└───
st   ─────────────────────────────────────────────────────────────────────────────────
159        λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id                   └──────────────┘        └────────┘             └─────────┘
src  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
typ  ─────┘ └───┘ └─┘└──────────────┘└─┘  └─┘└────────┘           └─────────┘└┘
doc  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
txt  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
par  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
pid  ─────┘ └───┘ └─┘                └─┘  └─┘                                └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
160      unfold glue_dist,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid            └────────┘
st   ───────────────────┘└─
161      have : infi (λp, dist x (Φ p) + dist z (Ψ p)) ≤ infi (λp, dist x (Φ p) + dist y (Ψ p)) + dist y z,
id                                                       └──┘                                  └──┘  
src      └─────┘      └─┘        └┘         └─┘ └──┘  └─┘        └┘         └─┘ └──┘ 
typ      └─────┘      └─┘        └┘         └─┘ └──┘  └─┘      └┘        └─┘ └──┘
doc      └─────┘      └─┘        └┘         └─┘ └──┘  └─┘        └┘         └─┘      
txt      └─────┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
par      └─────┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
pid      └───┘└┘      └─┘        └┘         └─┘       └─┘        └┘         └─┘      
st   ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
162      { have : infi (λp, dist x (Φ p) + dist y (Ψ p)) + dist y z =
src        └─────┘      └─┘        └┘         └─┘        
typ        └─────┘      └─┘        └┘         └─┘        
doc        └─────┘      └─┘        └┘         └─┘        
txt        └─────┘      └─┘        └┘         └─┘        
par        └─────┘      └─┘        └┘         └─┘        
pid        └───┘└┘      └─┘        └┘         └─┘        
st   ─────┘└──────────────────────────────────────────────────────────
163              infi ((λt, t + dist y z) ∘ (λp, dist x (Φ p) + dist y (Ψ p))),
id               └──┘                                        └──┘   
src  ───────────┘└──┘   └─┘        └┘   └─┘        └┘ └──┘    └─┘
typ  ───────────┘└──┘   └─┘       └┘   └─┘      └┘ └──┘  └─┘
doc  ───────────┘└──┘   └─┘        └┘   └─┘        └┘         └─┘
txt  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
par  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
pid  ───────────┘       └─┘        └┘   └─┘        └┘         └─┘
st   ────────────────────────────────────────────────────────────────────────┘└─
164        { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, t + dist y z)) _ (B _ _),
id                  └──────────────────────────────────────┘      └────────┘          └──┘        
src          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘  └──┘  └───┘  └───┘
typ          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘  └──┘└───┘ └───┘
doc          └─────┘└──────────────────────────────────────┘ └──┘└────────┘  └─┘        └───┘  └───┘
txt          └─────┘                                         └──┘            └─┘        └───┘  └───┘
par          └─────┘                                         └──┘            └─┘        └───┘  └───┘
pid                                                         └──┘            └─┘        └───┘  └───┘
st   ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
165          exact continuous_id.add continuous_const,
id                 └───────────────┘ └──────────────┘
src          └────┘└───────────────┘└──────────────┘
typ          └────┘└───────────────┘└──────────────┘
doc          └────┘                 
txt          └────┘                 
par          └────┘                 
pid                                
st   ───────────────────────────────────────────────┘└─
166          exact λx y hx, by simpa },
src          └────┘ └──────┘  └────┘
typ          └────┘ └──────┘  └────┘
doc          └────┘ └──────┘  └────┘
txt          └────┘ └──────┘  └────┘
par          └────┘ └──────┘  └────┘
pid                └──────┘  └─────┘
st   ────────────────────────┘└─────┘└┘
167        rw [this, comp],
id             └──┘  └──┘
src        └──┘    └┘└──┘
typ        └──┘└──┘└┘└──┘
doc        └──┘    └┘    
txt        └──┘    └┘    
par        └──┘    └┘    
pid          └┘    └┘    
st   ─────────────┘└────┘└──
168        refine cinfi_le_cinfi (B _ _) (λp, _),
id                └────────────┘  
src        └─────┘└────────────┘  └────┘  └───┘
typ        └─────┘└────────────┘ └────┘  └───┘
doc        └─────┘└────────────┘  └────┘  └───┘
txt        └─────┘                └────┘  └───┘
par        └─────┘                └────┘  └───┘
pid                              └────┘  └───┘
st   ──────────────────────────────────────────┘└─
169        calc
id         └──┘
src        └──┘
typ        └──┘
doc        └──┘
st   ───────────
170          dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + (dist y z + dist y (Ψ p)) :
st   ─────────────────────────────────────────────────────────────────────────────────
171            add_le_add (le_refl _) (dist_triangle_left _ _ _)
id             └────────┘  └─────┘     └────────────────┘
src            └────────┘  └─────┘     └────────────────┘
typ            └────────┘  └─────┘     └────────────────┘
st   ────────────────────────────────────────────────────────────
172          ... = dist x (Φ p) + dist y (Ψ p) + dist y z : by ring },
id                                           └──┘  
src                                              └──┘          └───┘
typ                                          └──┘        └───┘
doc                                                            └───┘
txt                                                            └───┘
par                                                            └───┘
pid                                                                
st   ────────────────────────────────────────────────────────┘└────┘└┘
173      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
174    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
175  | (inl x) (inr y) (inl z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
id              └─┘     └─┘       └──────────────────────────┘     └──┘
src             └─┘     └─┘       └──────────────────────────┘
typ             └─┘     └─┘       └──────────────────────────┘     └──┘
st                                                                        └─────
176      have : ∃a ∈ range (λp, dist x (Φ p) + dist y (Ψ p)), a < infi (λp, dist x (Φ p) + dist y (Ψ p)) + δ/2 :=
id                  └───┘                                       └──┘                   └──┘          
src      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘        └┘ └──┘    └─┘  └────
typ      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘      └┘ └──┘  └─┘ └────
doc      └─────┘ └──┘└───┘  └─┘        └┘         └┘   └──┘  └─┘        └┘         └─┘   └────
txt      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
par      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
pid      └───┘└┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
177        exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id         └──────────────────┘  └────────────┘            └──┘
src  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
typ  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
doc  ─────┘└──────────────────┘               └──┘   └──┘└──┘└┘└──────┘
txt  ─────┘                                   └──┘   └──┘    └┘└──────┘
par  ─────┘                                   └──┘   └──┘    └┘└──────┘
pid  ─────┘                                   └──┘   └───┘    └──────────┘
st   ────────────────────────────────────────────────┘└───────┘└────────┘└─
178      rcases this with ⟨a, arange, ha⟩,
id              └──┘
src      └─────┘    └───────────────────┘
typ      └─────┘└──┘└───────────────────┘
doc      └─────┘    └───────────────────┘
txt      └─────┘    └───────────────────┘
par      └─────┘    └───────────────────┘
pid                └───────────────────┘
st   ───────────────────────────────────┘└─
179      rcases mem_range.1 arange with ⟨p, pa⟩,
id              └───────┘   └────┘
src      └─────┘└───────┘└─┘      └───────────┘
typ      └─────┘└───────┘└─┘└────┘└───────────┘
doc      └─────┘         └─┘      └───────────┘
txt      └─────┘         └─┘      └───────────┘
par      └─────┘         └─┘      └───────────┘
pid                     └─┘      └───────────┘
st   ─────────────────────────────────────────┘└─
180      rw ← pa at ha,
id            └┘
src      └───┘  └────┘
typ      └───┘└┘└────┘
doc      └───┘  └────┘
txt      └───┘  └────┘
par      └───┘  └────┘
pid        └─┘  └────┘
st   ────────────────┘└─
181      have : ∃b ∈ range (λp, dist z (Φ p) + dist y (Ψ p)), b < infi (λp, dist z (Φ p) + dist y (Ψ p)) + δ/2 :=
id                  └───┘                                       └──┘                   └──┘          
src      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘        └┘ └──┘    └─┘   └────
typ      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘      └┘ └──┘  └─┘  └────
doc      └─────┘ └──┘└───┘  └─┘        └┘         └┘   └──┘  └─┘        └┘         └─┘   └────
txt      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
par      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
pid      └───┘└┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
182        exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id         └──────────────────┘  └────────────┘            └──┘
src  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
typ  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
doc  ─────┘└──────────────────┘               └──┘   └──┘└──┘└┘└──────┘
txt  ─────┘                                   └──┘   └──┘    └┘└──────┘
par  ─────┘                                   └──┘   └──┘    └┘└──────┘
pid  ─────┘                                   └──┘   └───┘    └──────────┘
st   ────────────────────────────────────────────────┘└───────┘└────────┘└─
183      rcases this with ⟨b, brange, hb⟩,
id              └──┘
src      └─────┘    └───────────────────┘
typ      └─────┘└──┘└───────────────────┘
doc      └─────┘    └───────────────────┘
txt      └─────┘    └───────────────────┘
par      └─────┘    └───────────────────┘
pid                └───────────────────┘
st   ───────────────────────────────────┘└─
184      rcases mem_range.1 brange with ⟨q, qb⟩,
id              └───────┘   └────┘
src      └─────┘└───────┘└─┘      └───────────┘
typ      └─────┘└───────┘└─┘└────┘└───────────┘
doc      └─────┘         └─┘      └───────────┘
txt      └─────┘         └─┘      └───────────┘
par      └─────┘         └─┘      └───────────┘
pid                     └─┘      └───────────┘
st   ─────────────────────────────────────────┘└─
185      rw ← qb at hb,
id            └┘
src      └───┘  └────┘
typ      └───┘└┘└────┘
doc      └───┘  └────┘
txt      └───┘  └────┘
par      └───┘  └────┘
pid        └─┘  └────┘
st   ────────────────┘└─
186      have : dist (Φ p) (Φ q) ≤ dist (Ψ p) (Ψ q) + 2 * ε,
id                                └──┘                
src      └─────┘       └┘   └┘ └──┘   └┘   └┘ └─┘ 
typ      └─────┘       └┘  └┘ └──┘  └┘ └┘ └─┘ 
doc      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
txt      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
par      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
pid      └───┘└┘       └┘   └┘        └┘   └┘ └─┘ 
st   ─────────────────────────────────────────────────────┘└─
187        { have := le_trans (le_abs_self _) (H p q), by linarith },
id                   └──────┘  └─────────┘       
src          └──────┘└──────┘ └─────────┘└──┘         └───────┘
typ          └──────┘└──────┘ └─────────┘└──┘      └───────┘
doc          └──────┘                    └──┘         └───────┘
txt          └──────┘                    └──┘         └───────┘
par          └──────┘                    └──┘         └───────┘
pid          └───┘└─┘                    └──┘                 
st   ───────┘└──────────────────────────────────────┘              └┘
188      calc dist x z ≤ dist x (Φ p) + dist (Φ p) (Φ q) + dist (Φ q) z : dist_triangle4 _ _ _ _
id       └──┘                                            └──┘        └────────────┘
src      └──┘                                              └──┘           └────────────┘
typ      └──┘                                            └──┘        └────────────┘
doc      └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────
189        ... ≤ dist x (Φ p) + dist (Ψ p) (Ψ q) + dist z (Φ q) + 2 * ε : by rw [dist_comm z]; linarith
id                                                                             └───────┘ 
src                                                                          └──┘└───────┘   └────────
typ                                                                        └──┘└───────┘  └────────
doc                                                                          └──┘            └────────
txt                                                                          └──┘            └────────
par                                                                          └──┘            └────────
pid                                                                            └┘                    
st   ──────────────────────────────────────────────────────────────────────┘└──────────────┘└──────────
190        ... ≤ dist x (Φ p) + (dist y (Ψ p) + dist y (Ψ q)) + dist z (Φ q) + 2 * ε :
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└───────────────────────────────────────────────────────────────────────────
191          add_le_add (add_le_add (add_le_add (le_refl _) (dist_triangle_left _ _ _)) (le_refl _)) (le_refl _)
id                                   └────────┘              └────────────────┘                       └─────┘
src                                  └────────┘              └────────────────┘                       └─────┘
typ                                  └────────┘              └────────────────┘                       └─────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────
192        ... ≤ (infi (λp, dist x (Φ p) + dist y (Ψ p)) + ε) + (infi (λp, dist z (Φ p) + dist y (Ψ p)) + ε) + δ :
id                                                              └──┘                                        
src                                                              └──┘
typ                                                             └──┘                                        
doc                                                              └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
193          by linarith
src             └────────
typ             └────────
doc             └────────
txt             └────────
par             └────────
pid                     
st   ─────────┘└─────────
194    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
195  | (inr x) (inl y) (inr z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
id              └─┘     └─┘       └──────────────────────────┘     └──┘
src             └─┘     └─┘       └──────────────────────────┘
typ             └─┘     └─┘       └──────────────────────────┘     └──┘
st                                                                        └─────
196      have : ∃a ∈ range (λp, dist y (Φ p) + dist x (Ψ p)), a < infi (λp, dist y (Φ p) + dist x (Ψ p)) + δ/2 :=
id                  └───┘                                       └──┘                   └──┘          
src      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘        └┘ └──┘    └─┘   └────
typ      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘      └┘ └──┘  └─┘  └────
doc      └─────┘ └──┘└───┘  └─┘        └┘         └┘   └──┘  └─┘        └┘         └─┘   └────
txt      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
par      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
pid      └───┘└┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
197        exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id         └──────────────────┘  └────────────┘            └──┘
src  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
typ  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
doc  ─────┘└──────────────────┘               └──┘   └──┘└──┘└┘└──────┘
txt  ─────┘                                   └──┘   └──┘    └┘└──────┘
par  ─────┘                                   └──┘   └──┘    └┘└──────┘
pid  ─────┘                                   └──┘   └───┘    └──────────┘
st   ────────────────────────────────────────────────┘└───────┘└────────┘└─
198      rcases this with ⟨a, arange, ha⟩,
id              └──┘
src      └─────┘    └───────────────────┘
typ      └─────┘└──┘└───────────────────┘
doc      └─────┘    └───────────────────┘
txt      └─────┘    └───────────────────┘
par      └─────┘    └───────────────────┘
pid                └───────────────────┘
st   ───────────────────────────────────┘└─
199      rcases mem_range.1 arange with ⟨p, pa⟩,
id              └───────┘   └────┘
src      └─────┘└───────┘└─┘      └───────────┘
typ      └─────┘└───────┘└─┘└────┘└───────────┘
doc      └─────┘         └─┘      └───────────┘
txt      └─────┘         └─┘      └───────────┘
par      └─────┘         └─┘      └───────────┘
pid                     └─┘      └───────────┘
st   ─────────────────────────────────────────┘└─
200      rw ← pa at ha,
id            └┘
src      └───┘  └────┘
typ      └───┘└┘└────┘
doc      └───┘  └────┘
txt      └───┘  └────┘
par      └───┘  └────┘
pid        └─┘  └────┘
st   ────────────────┘└─
201      have : ∃b ∈ range (λp, dist y (Φ p) + dist z (Ψ p)), b < infi (λp, dist y (Φ p) + dist z (Ψ p)) + δ/2 :=
id                  └───┘                                       └──┘                   └──┘          
src      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘        └┘ └──┘    └─┘   └────
typ      └─────┘└──┘└───┘  └─┘        └┘         └┘  └──┘  └─┘      └┘ └──┘  └─┘  └────
doc      └─────┘ └──┘└───┘  └─┘        └┘         └┘   └──┘  └─┘        └┘         └─┘   └────
txt      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
par      └─────┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
pid      └───┘└┘ └──┘       └─┘        └┘         └┘         └─┘        └┘         └─┘   └────
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
202        exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id         └──────────────────┘  └────────────┘            └──┘
src  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
typ  ─────┘└──────────────────┘ └────────────┘└──┘   └──┘└──┘└┘└──────┘
doc  ─────┘└──────────────────┘               └──┘   └──┘└──┘└┘└──────┘
txt  ─────┘                                   └──┘   └──┘    └┘└──────┘
par  ─────┘                                   └──┘   └──┘    └┘└──────┘
pid  ─────┘                                   └──┘   └───┘    └──────────┘
st   ────────────────────────────────────────────────┘└───────┘└────────┘└─
203      rcases this with ⟨b, brange, hb⟩,
id              └──┘
src      └─────┘    └───────────────────┘
typ      └─────┘└──┘└───────────────────┘
doc      └─────┘    └───────────────────┘
txt      └─────┘    └───────────────────┘
par      └─────┘    └───────────────────┘
pid                └───────────────────┘
st   ───────────────────────────────────┘└─
204      rcases mem_range.1 brange with ⟨q, qb⟩,
id              └───────┘   └────┘
src      └─────┘└───────┘└─┘      └───────────┘
typ      └─────┘└───────┘└─┘└────┘└───────────┘
doc      └─────┘         └─┘      └───────────┘
txt      └─────┘         └─┘      └───────────┘
par      └─────┘         └─┘      └───────────┘
pid                     └─┘      └───────────┘
st   ─────────────────────────────────────────┘└─
205      rw ← qb at hb,
id            └┘
src      └───┘  └────┘
typ      └───┘└┘└────┘
doc      └───┘  └────┘
txt      └───┘  └────┘
par      └───┘  └────┘
pid        └─┘  └────┘
st   ────────────────┘└─
206      have : dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ q) + 2 * ε,
id                                └──┘                
src      └─────┘       └┘   └┘ └──┘   └┘   └┘ └─┘ 
typ      └─────┘       └┘  └┘ └──┘  └┘ └┘ └─┘ 
doc      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
txt      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
par      └─────┘       └┘   └┘        └┘   └┘ └─┘ 
pid      └───┘└┘       └┘   └┘        └┘   └┘ └─┘ 
st   ─────────────────────────────────────────────────────┘└─
207        { have := le_trans (neg_le_abs_self _) (H p q), by linarith },
id                   └──────┘  └─────────────┘       
src          └──────┘└──────┘ └─────────────┘└──┘         └───────┘
typ          └──────┘└──────┘ └─────────────┘└──┘      └───────┘
doc          └──────┘                        └──┘         └───────┘
txt          └──────┘                        └──┘         └───────┘
par          └──────┘                        └──┘         └───────┘
pid          └───┘└─┘                        └──┘                 
st   ───────┘└──────────────────────────────────────────┘              └┘
208      calc dist x z ≤ dist x (Ψ p) + dist (Ψ p) (Ψ q) + dist (Ψ q) z : dist_triangle4 _ _ _ _
id       └──┘                                            └──┘        └────────────┘
src      └──┘                                              └──┘           └────────────┘
typ      └──┘                                            └──┘        └────────────┘
doc      └──┘
st   ────────────────────────────────────────────────────────────────────────────────────────────
209        ... ≤ dist x (Ψ p) + dist (Φ p) (Φ q) + dist z (Ψ q) + 2 * ε : by rw [dist_comm z]; linarith
id                                                                             └───────┘ 
src                                                                          └──┘└───────┘   └────────
typ                                                                        └──┘└───────┘  └────────
doc                                                                          └──┘            └────────
txt                                                                          └──┘            └────────
par                                                                          └──┘            └────────
pid                                                                            └┘                    
st   ──────────────────────────────────────────────────────────────────────┘└──────────────┘└──────────
210        ... ≤ dist x (Ψ p) + (dist y (Φ p) + dist y (Φ q)) + dist z (Ψ q) + 2 * ε :
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└───────────────────────────────────────────────────────────────────────────
211          add_le_add (add_le_add (add_le_add (le_refl _) (dist_triangle_left _ _ _)) (le_refl _)) (le_refl _)
id                                   └────────┘              └────────────────┘                       └─────┘
src                                  └────────┘              └────────────────┘                       └─────┘
typ                                  └────────┘              └────────────────┘                       └─────┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────
212        ... ≤ (infi (λp, dist y (Φ p) + dist x (Ψ p)) + ε) + (infi (λp, dist y (Φ p) + dist z (Ψ p)) + ε) + δ :
id                                                              └──┘                                        
src                                                              └──┘
typ                                                             └──┘                                        
doc                                                              └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
213          by linarith
src             └────────
typ             └────────
doc             └────────
txt             └────────
par             └────────
pid                     
st   ─────────┘└─────────
214    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
215  
216  private lemma glue_eq_of_dist_eq_zero (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (ε0 : 0 < ε) :
id                                                                             
src                                                                               
typ                                                                            
217    ∀p q : α ⊕ β, glue_dist Φ Ψ ε p q = 0 → p = q
id               └───────┘             
src                 └───────┘                  
typ              └───────┘             
doc                  └───────┘
218  | (inl x) (inl y) h := by rw eq_of_dist_eq_zero h
id              └─┘               └────────────────┘ 
src             └─┘            └─┘└────────────────┘ 
typ             └─┘            └─┘└────────────────┘
doc                            └─┘                   
txt                            └─┘                   
par                            └─┘                   
pid                                                 
st                            └───────────────────────┘
219  | (inl x) (inr y) h := begin
id      └─┘     └─┘
src     └─┘     └─┘
typ     └─┘     └─┘
st                          └─────
220      have : 0 ≤ infi (λp, dist x (Φ p) + dist y (Ψ p)) :=
id                 └──┘                  └──┘   
src      └───────┘└──┘  └─┘        └┘└──┘    └─────
typ      └───────┘└──┘  └─┘      └┘└──┘  └─────
doc      └───────┘ └──┘  └─┘        └┘         └─────
txt      └───────┘       └─┘        └┘         └─────
par      └───────┘       └─┘        └┘         └─────
pid      └───┘└──┘       └─┘        └┘         └┘└───
st   ─────────────────────────────────────────────────────────
221        le_cinfi (λp, by simpa using add_le_add (@dist_nonneg _ _ x _) (@dist_nonneg _ _ y _)),
id         └──────┘                     └────────┘                         └─────────┘     
src  ─────┘└──────┘  └─┘  └──────────┘└────────┘             └───┘ └──┘  └─────────┘└───┘ └─┘
typ  ─────┘└──────┘  └─┘  └──────────┘└────────┘             └───┘└──┘  └─────────┘└───┘└─┘
doc  ─────┘└──────┘  └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
txt  ─────┘          └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
par  ─────┘          └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
pid  ─────┘          └─┘  └───────────┘                       └───┘ └──┘             └───┘ └──┘
st   ─────────────────────┘└───────────────────────────────────────────────────────────────────┘└─
222      have : 0 + ε ≤ glue_dist Φ Ψ ε (inl x) (inr y) := add_le_add this (le_refl ε),
id                      └───────┘     └─┘    └─┘      └────────┘ └──┘  └─────┘ 
src      └───────┘   └───────┘    └─┘ └┘ └─┘ └───┘└────────┘     └─────┘ 
typ      └───────┘   └───────┘ └─┘└┘ └─┘└───┘└────────┘└──┘ └─────┘
doc      └───────┘   └───────┘        └┘     └───┘                       
txt      └───────┘                    └┘     └───┘                       
par      └───────┘                    └┘     └───┘                       
pid      └───┘└──┘                    └┘     └──┘                       
st   ────────────────────────────────────────────────────────────────────────────────┘└─
223      exfalso,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
st   ──────────┘└─
224      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
225    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
226  | (inr x) (inl y) h := begin
id      └─┘     └─┘
src     └─┘     └─┘
typ     └─┘     └─┘
st                          └─────
227      have : 0 ≤ infi (λp, dist y (Φ p) + dist x (Ψ p)) :=
id                  └──┘                   └──┘   
src      └───────┘ └──┘  └─┘        └┘ └──┘    └─────
typ      └───────┘ └──┘  └─┘      └┘ └──┘  └─────
doc      └───────┘ └──┘  └─┘        └┘         └─────
txt      └───────┘       └─┘        └┘         └─────
par      └───────┘       └─┘        └┘         └─────
pid      └───┘└──┘       └─┘        └┘         └┘└───
st   ─────────────────────────────────────────────────────────
228        le_cinfi (λp, by simpa using add_le_add (@dist_nonneg _ _ x _) (@dist_nonneg _ _ y _)),
id         └──────┘                     └────────┘                         └─────────┘     
src  ─────┘└──────┘  └─┘  └──────────┘└────────┘             └───┘ └──┘  └─────────┘└───┘ └─┘
typ  ─────┘└──────┘  └─┘  └──────────┘└────────┘             └───┘└──┘  └─────────┘└───┘└─┘
doc  ─────┘└──────┘  └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
txt  ─────┘          └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
par  ─────┘          └─┘  └──────────┘                       └───┘ └──┘             └───┘ └─┘
pid  ─────┘          └─┘  └───────────┘                       └───┘ └──┘             └───┘ └──┘
st   ─────────────────────┘└───────────────────────────────────────────────────────────────────┘└─
229      have : 0 + ε ≤ glue_dist Φ Ψ ε (inr x) (inl y) := add_le_add this (le_refl ε),
id                      └───────┘     └─┘    └─┘      └────────┘ └──┘  └─────┘ 
src      └───────┘   └───────┘    └─┘ └┘ └─┘ └───┘└────────┘     └─────┘ 
typ      └───────┘   └───────┘ └─┘└┘ └─┘└───┘└────────┘└──┘ └─────┘
doc      └───────┘   └───────┘        └┘     └───┘                       
txt      └───────┘                    └┘     └───┘                       
par      └───────┘                    └┘     └───┘                       
pid      └───┘└──┘                    └┘     └──┘                       
st   ────────────────────────────────────────────────────────────────────────────────┘└─
230      exfalso,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
st   ──────────┘└─
231      linarith
src      └────────
typ      └────────
doc      └────────
txt      └────────
par      └────────
pid              
st   ─────────────
232    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
233  | (inr x) (inr y) h := by rw eq_of_dist_eq_zero h
id              └─┘               └────────────────┘ 
src             └─┘            └─┘└────────────────┘ 
typ             └─┘            └─┘└────────────────┘
doc                            └─┘                   
txt                            └─┘                   
par                            └─┘                   
pid                                                 
st                            └────────────────────────
234  
src  
typ  
doc  
txt  
par  
pid  
st   
235  /-- Given two maps Φ and Ψ intro metric spaces α and β such that the distances between Φ p and Φ q,
236  and between Ψ p and Ψ q, coincide up to 2 ε where ε > 0, one can almost glue the two spaces α
237  and β along the images of Φ and Ψ, so that Φ p and Ψ p are at distance ε. -/
238  def glue_metric_approx (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (ε0 : 0 < ε)
id                                                              
src                                                                
typ                                                             
239    (H : ∀p q, abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε) : metric_space (α ⊕ β) :=
id              └─┘  └──┘          └──┘                  └──────────┘    
src               └─┘  └──┘              └──┘                       └──────────┘    
typ             └─┘  └──┘          └──┘                  └──────────┘    
doc                                                                    └──────────┘
240  { dist               := glue_dist Φ Ψ ε,
id                          └───────┘   
src                         └───────┘
typ                         └───────┘   
doc                          └───────┘
241    dist_self          := glue_dist_self Φ Ψ ε,
id                           └────────────┘   
src                          └────────────┘
typ                          └────────────┘   
242    dist_comm          := glue_dist_comm Φ Ψ ε,
id                           └────────────┘   
src                          └────────────┘
typ                          └────────────┘   
243    dist_triangle      := glue_dist_triangle Φ Ψ ε H,
id                           └────────────────┘    
src                          └────────────────┘
typ                          └────────────────┘    
244    eq_of_dist_eq_zero := glue_eq_of_dist_eq_zero Φ Ψ ε ε0 }
id                           └─────────────────────┘    └┘
src                          └─────────────────────┘
typ                          └─────────────────────┘    └┘
245  
246  end approx_gluing
247  
248  section sum
249  /- A particular case of the previous construction is when one uses basepoints in α and β and one
250  glues only along the basepoints, putting them at distance 1. We give a direct definition of
251  the distance, without infi, as it is easier to use in applications, and show that it is equal to
252  the gluing distance defined above to take advantage of the lemmas we have already proved. -/
253  
254  variables [metric_space α] [metric_space β] [inhabited α] [inhabited β]
id              └──────────┘     └──────────┘     └───────┘     └───────┘
src             └──────────┘     └──────────┘     └───────┘     └───────┘
typ             └──────────┘     └──────────┘     └───────┘     └───────┘
doc             └──────────┘     └──────────┘
255  open sum (inl inr)
256  
257  /- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
258  with each factor.
259  If the two spaces are bounded, one can say for instance that each point in the first is at distance
260  `diam α + diam β + 1` of each point in the second.
261  Instead, we choose a construction that works for unbounded spaces, but requires basepoints.
262  We embed isometrically each factor, set the basepoints at distance 1,
263  arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
264  their respective basepoints, plus the distance 1 between the basepoints.
265  Since there is an arbitrary choice in this construction, it is not an instance by default. -/
266  
267  def sum.dist : α ⊕ β → α ⊕ β → ℝ
id                           
src                               
typ                          
268  | (inl a) (inl a') := dist a a'
id             └─┘ └┘     └──┘
src             └─┘        └──┘
typ            └─┘ └┘     └──┘
269  | (inr b) (inr b') := dist b b'
id             └─┘ └┘     └──┘
src             └─┘        └──┘
typ            └─┘ └┘     └──┘
270  | (inl a) (inr b)  := dist a (default α) + 1 + dist (default β) b
id      └─┘    └─┘       └──┘    └─────┘       └──┘  └─────┘ 
src     └─┘     └─┘        └──┘    └─────┘        └──┘  └─────┘
typ     └─┘    └─┘       └──┘    └─────┘       └──┘  └─────┘ 
271  | (inr b) (inl a)  := dist b (default β) + 1 + dist (default α) a
id      └─┘    └─┘       └──┘    └─────┘       └──┘  └─────┘ 
src     └─┘     └─┘        └──┘    └─────┘        └──┘  └─────┘
typ     └─┘    └─┘       └──┘    └─────┘       └──┘  └─────┘ 
272  
273  lemma sum.dist_eq_glue_dist {p q : α ⊕ β} :
id                                        
src                                       
typ                                       
274    sum.dist p q = glue_dist (λ_ : unit, default α) (λ_ : unit, default β) 1 p q :=
id     └──────┘    └───────┘       └──┘  └─────┘         └──┘  └─────┘      
src    └──────┘      └───────┘       └──┘  └─────┘          └──┘  └─────┘
typ    └──────┘    └───────┘       └──┘  └─────┘         └──┘  └─────┘      
doc                   └───────┘       └──┘                   └──┘
275  by cases p; cases q; refl <|> simp [sum.dist, glue_dist, dist_comm]
id                                     └──────┘  └───────┘  └───────┘
src     └────┘   └────┘   └───┘    └────┘└──────┘└┘└───────┘└┘└───────┘└─
typ     └────┘  └────┘  └───┘    └────┘└──────┘└┘└───────┘└┘└───────┘└─
doc     └────┘   └────┘   └───┘    └────┘        └┘└───────┘└┘         └─
txt     └────┘   └────┘   └───┘    └────┘        └┘         └┘         └─
par     └────┘   └────┘   └───┘    └────┘        └┘         └┘         └─
pid                                         └┘         └┘         
st     └─────────────────────────────────────────────────────────────────
276  
src  
typ  
doc  
txt  
par  
pid  
st   
277  private lemma sum.dist_comm (x y : α ⊕ β) : sum.dist x y = sum.dist y x :=
id                                            └──────┘    └──────┘  
src                                             └──────┘      └──────┘
typ                                           └──────┘    └──────┘  
278  by cases x; cases y; simp only [sum.dist, dist_comm, add_comm, add_left_comm]
id                                 └──────┘  └───────┘  └──────┘  └───────────┘
src     └────┘   └────┘   └─────────┘└──────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
typ     └────┘  └────┘  └─────────┘└──────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
doc     └────┘   └────┘   └─────────┘        └┘         └┘        └┘             └─
txt     └────┘   └────┘   └─────────┘        └┘         └┘        └┘             └─
par     └────┘   └────┘   └─────────┘        └┘         └┘        └┘             └─
pid                         └──┘└┘        └┘         └┘        └┘             
st     └───────────────────────────────────────────────────────────────────────────
279  
src  
typ  
doc  
txt  
par  
pid  
st   
280  lemma sum.one_dist_le {x : α} {y : β} : 1 ≤ sum.dist (inl x) (inr y) :=
id                                            └──────┘  └─┘    └─┘ 
src                                             └──────┘  └─┘     └─┘
typ                                           └──────┘  └─┘    └─┘ 
281  le_trans (le_add_of_nonneg_right dist_nonneg) $
id   └──────┘  └────────────────────┘ └─────────┘
src  └──────┘  └────────────────────┘ └─────────┘
typ  └──────┘  └────────────────────┘ └─────────┘
282  add_le_add_right (le_add_of_nonneg_left dist_nonneg) _
id   └──────────────┘  └───────────────────┘ └─────────┘
src  └──────────────┘  └───────────────────┘ └─────────┘
typ  └──────────────┘  └───────────────────┘ └─────────┘
283  
284  lemma sum.one_dist_le' {x : α} {y : β} : 1 ≤ sum.dist (inr y) (inl x) :=
id                                             └──────┘  └─┘    └─┘ 
src                                              └──────┘  └─┘     └─┘
typ                                            └──────┘  └─┘    └─┘ 
285  by rw sum.dist_comm; exact sum.one_dist_le
id         └───────────┘        └─────────────┘
src     └─┘└───────────┘  └────┘└─────────────┘
typ     └─┘└───────────┘  └────┘└─────────────┘
doc     └─┘               └────┘               
txt     └─┘               └────┘               
par     └─┘               └────┘               
pid                                          
st     └────────────────────────────────────────
286  
src  
typ  
doc  
txt  
par  
pid  
st   
287  private lemma sum.mem_uniformity (s : set ((α ⊕ β) × (α ⊕ β))) :
id                                         └─┘           
src                                        └─┘             
typ                                        └─┘           
288    s ∈ (@uniformity (α ⊕ β) _).sets ↔ ∃ ε > 0, ∀ a b, sum.dist a b < ε → (a, b) ∈ s :=
id         └────────┘        └──┘              └──────┘            
src         └────────┘          └──┘                 └──────┘                
typ        └────────┘        └──┘              └──────┘            
doc          └────────┘
289  begin
st   └─────
290    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
291    { rintro ⟨hsα, hsβ⟩,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid            └─────────┘
st   ───┘└───────────────┘└─
292      rcases mem_uniformity_dist.1 hsα with ⟨εα, εα0, hα⟩,
id              └─────────────────┘   └─┘
src      └─────┘└─────────────────┘└─┘   └─────────────────┘
typ      └─────┘└─────────────────┘└─┘└─┘└─────────────────┘
doc      └─────┘                   └─┘   └─────────────────┘
txt      └─────┘                   └─┘   └─────────────────┘
par      └─────┘                   └─┘   └─────────────────┘
pid                               └─┘   └─────────────────┘
st   ──────────────────────────────────────────────────────┘└─
293      rcases mem_uniformity_dist.1 hsβ with ⟨εβ, εβ0, hβ⟩,
id              └─────────────────┘   └─┘
src      └─────┘└─────────────────┘└─┘   └─────────────────┘
typ      └─────┘└─────────────────┘└─┘└─┘└─────────────────┘
doc      └─────┘                   └─┘   └─────────────────┘
txt      └─────┘                   └─┘   └─────────────────┘
par      └─────┘                   └─┘   └─────────────────┘
pid                               └─┘   └─────────────────┘
st   ──────────────────────────────────────────────────────┘└─
294      refine ⟨min (min εα εβ) 1, lt_min (lt_min εα0 εβ0) zero_lt_one, _⟩,
id                    └─┘ └┘ └┘             └────┘ └─┘ └─┘  └─────────┘
src      └─────┘     └─┘    └───┘       └────┘      └┘└─────────┘└──┘
typ      └─────┘     └─┘└┘└┘└───┘       └────┘└─┘└─┘└┘└─────────┘└──┘
doc      └─────┘            └───┘                   └┘           └──┘
txt      └─────┘            └───┘                   └┘           └──┘
par      └─────┘            └───┘                   └┘           └──┘
pid                        └───┘                   └┘           └──┘
st   ─────────────────────────────────────────────────────────────────────┘└─
295      rintro (a|a) (b|b) h,
src      └──────────────────┘
typ      └──────────────────┘
doc      └──────────────────┘
txt      └──────────────────┘
par      └──────────────────┘
pid            └────────────┘
st   ───────────────────────┘└─
296      { exact hα (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _))) },
id               └┘  └────────────┘   └──────┘                    └─────────┘
src        └────┘   └────────────┘  └──────┘            └────┘ └─────────┘└──────┘
typ        └────┘└┘ └────────────┘ └──────┘            └────┘ └─────────┘└──────┘
doc        └────┘                                       └────┘            └──────┘
txt        └────┘                                       └────┘            └──────┘
par        └────┘                                       └────┘            └──────┘
pid                                                    └────┘            └─────┘
st   ─────┘└─────────────────────────────────────────────────────────────────────────┘└┘
297      { cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) sum.one_dist_le },
id               └──────────┘  └────────────┘   └──────────┘       └─────────────┘
src        └────┘└──────────┘ └────────────┘  └──────────┘└─────┘└─────────────┘
typ        └────┘└──────────┘ └────────────┘ └──────────┘└─────┘└─────────────┘
doc        └────┘                                         └─────┘               
txt        └────┘                                         └─────┘               
par        └────┘                                         └─────┘               
pid                                                      └─────┘               
st   ─────┘└───────────────────────────────────────────────────────────────────────┘└┘
298      { cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) sum.one_dist_le' },
id               └──────────┘  └────────────┘   └──────────┘       └──────────────┘
src        └────┘└──────────┘ └────────────┘  └──────────┘└─────┘└──────────────┘
typ        └────┘└──────────┘ └────────────┘ └──────────┘└─────┘└──────────────┘
doc        └────┘                                         └─────┘                
txt        └────┘                                         └─────┘                
par        └────┘                                         └─────┘                
pid                                                      └─────┘                
st   ─────┘└────────────────────────────────────────────────────────────────────────┘└┘
299      { exact hβ (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _))) } },
id               └┘  └────────────┘   └──────┘  └─────────┘       └──────────┘
src        └────┘   └────────────┘  └──────┘ └─────────┘└────┘ └──────────┘└──────┘
typ        └────┘└┘ └────────────┘ └──────┘ └─────────┘└────┘ └──────────┘└──────┘
doc        └────┘                                       └────┘             └──────┘
txt        └────┘                                       └────┘             └──────┘
par        └────┘                                       └────┘             └──────┘
pid                                                    └────┘             └─────┘
st   ─────────────────────────────────────────────────────────────────────────────────┘└──┘
300    { rintro ⟨ε, ε0, H⟩,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid            └─────────┘
st   ────────────────────┘└─
301      split; rw [filter.mem_map, mem_uniformity_dist];
id                  └────────────┘  └─────────────────┘
src      └───┘  └──┘└────────────┘└┘└─────────────────┘
typ      └───┘  └──┘└────────────┘└┘└─────────────────┘
doc      └───┘  └──┘              └┘                   
txt      └───┘  └──┘              └┘                   
par      └───┘  └──┘              └┘                   
pid               └┘              └┘                   
st   ──────────────┘└────────────┘└───────────────────┘└─
302        exact ⟨ε, ε0, λ x y h, H _ _ (by exact h)⟩ }
id                  └┘                          
src        └────┘  └┘  └┘ └──────┘ └───┘   └─────┘ └─┘
typ        └────┘ └┘└┘└┘ └──────┘└───┘   └─────┘└─┘
doc        └────┘  └┘  └┘ └──────┘ └───┘   └─────┘ └─┘
txt        └────┘  └┘  └┘ └──────┘ └───┘   └─────┘ └─┘
par        └────┘  └┘  └┘ └──────┘ └───┘   └─────┘ └─┘
pid               └┘  └┘ └──────┘ └───┘   └─────┘ └┘
st   ─────────────────────────────────────┘└──────┘└─┘└─
303  end
st   ──┘
304  
305  /-- The distance on the disjoint union indeed defines a metric space. All the distance properties follow from our
306  choice of the distance. The harder work is to show that the uniform structure defined by the distance coincides
307  with the disjoint union uniform structure. -/
308  def metric_space_sum : metric_space (α ⊕ β) :=
id                          └──────────┘    
src                         └──────────┘    
typ                         └──────────┘    
doc                         └──────────┘
309  { dist               := sum.dist,
id                          └──────┘
src                         └──────┘
typ                         └──────┘
310    dist_self          := λx, by cases x; simp only [sum.dist, dist_self],
id                                                    └──────┘  └───────┘
src                                 └────┘   └─────────┘└──────┘└┘└───────┘
typ                                └────┘  └─────────┘└──────┘└┘└───────┘
doc                                 └────┘   └─────────┘        └┘         
txt                                 └────┘   └─────────┘        └┘         
par                                 └────┘   └─────────┘        └┘         
pid                                             └──┘└┘        └┘         
st                                 └───────────────────────────────────────┘
311    dist_comm          := sum.dist_comm,
id                           └───────────┘
src                          └───────────┘
typ                          └───────────┘
312    dist_triangle      := λp q r,
id                              
typ                             
313      by simp only [dist, sum.dist_eq_glue_dist]; exact glue_dist_triangle _ _ _ (by simp; norm_num) _ _ _,
id                           └───────────────────┘         └────────────────┘
src         └─────────┘    └┘└───────────────────┘  └────┘└────────────────┘└─────┘   └──┘└┘└──────┘└─────┘
typ         └─────────┘    └┘└───────────────────┘  └────┘└────────────────┘└─────┘   └──┘└┘└──────┘└─────┘
doc         └─────────┘    └┘                       └────┘                  └─────┘   └──┘└┘└──────┘└─────┘
txt         └─────────┘    └┘                       └────┘                  └─────┘   └──┘└┘└──────┘└─────┘
par         └─────────┘    └┘                       └────┘                  └─────┘   └──┘└┘└──────┘└─────┘
pid             └──┘└┘    └┘                                              └─────┘   └────────────────────┘
st         └──────────────────────────────────────────────────────────────────────────┘└─────────────┘└─────┘
314    eq_of_dist_eq_zero := λp q,
id                             
typ                            
315      by simp only [dist, sum.dist_eq_glue_dist]; exact glue_eq_of_dist_eq_zero _ _ _ zero_lt_one _ _,
id                           └───────────────────┘         └─────────────────────┘       └─────────┘
src         └─────────┘    └┘└───────────────────┘  └────┘└─────────────────────┘└─────┘└─────────┘└──┘
typ         └─────────┘    └┘└───────────────────┘  └────┘└─────────────────────┘└─────┘└─────────┘└──┘
doc         └─────────┘    └┘                       └────┘                       └─────┘           └──┘
txt         └─────────┘    └┘                       └────┘                       └─────┘           └──┘
par         └─────────┘    └┘                       └────┘                       └─────┘           └──┘
pid             └──┘└┘    └┘                                                   └─────┘           └──┘
st         └───────────────────────────────────────────────────────────────────────────────────────────┘
316    to_uniform_space   := sum.uniform_space,
id                           └───────────────┘
src                          └───────────────┘
typ                          └───────────────┘
317    uniformity_dist    := uniformity_dist_of_mem_uniformity _ _ sum.mem_uniformity }
id                           └───────────────────────────────┘     └────────────────┘
src                          └───────────────────────────────┘     └────────────────┘
typ                          └───────────────────────────────┘     └────────────────┘
doc                          └───────────────────────────────┘
318  
319  local attribute [instance] metric_space_sum
id                              └──────────────┘
src                             └──────────────┘
typ                             └──────────────┘
doc                             └──────────────┘
320  
321  lemma sum.dist_eq {x y : α ⊕ β} : dist x y = sum.dist x y := rfl
id                                  └──┘    └──────┘      └─┘
src                                   └──┘      └──────┘        └─┘
typ                                 └──┘    └──────┘      └─┘
322  
323  /-- The left injection of a space in a disjoint union in an isometry -/
324  lemma isometry_on_inl : isometry (sum.inl : α → (α ⊕ β)) :=
id                           └──────┘  └─────┘         
src                          └──────┘  └─────┘          
typ                          └──────┘  └─────┘         
doc                          └──────┘
325  isometry_emetric_iff_metric.2 $ λx y, rfl
id   └─────────────────────────┘        └─┘
src  └─────────────────────────┘          └─┘
typ  └─────────────────────────┘        └─┘
doc  └─────────────────────────┘
326  
327  /-- The right injection of a space in a disjoint union in an isometry -/
328  lemma isometry_on_inr : isometry (sum.inr : β → (α ⊕ β)) :=
id                           └──────┘  └─────┘         
src                          └──────┘  └─────┘          
typ                          └──────┘  └─────┘         
doc                          └──────┘
329  isometry_emetric_iff_metric.2 $ λx y, rfl
id   └─────────────────────────┘        └─┘
src  └─────────────────────────┘          └─┘
typ  └─────────────────────────┘        └─┘
doc  └─────────────────────────┘
330  
331  end sum
332  
333  section gluing
334  /- Exact gluing of two metric spaces along isometric subsets. -/
335  
336  variables [nonempty γ] [metric_space γ] [metric_space α] [metric_space β]
id              └──────┘     └──────────┘     └──────────┘     └──────────┘
src             └──────┘     └──────────┘     └──────────┘     └──────────┘
typ             └──────┘     └──────────┘     └──────────┘     └──────────┘
doc                          └──────────┘     └──────────┘     └──────────┘
337            {Φ : γ → α} {Ψ : γ → β} {ε : ℝ}
id                                          
src                                         
typ                                         
338  open sum (inl inr)
339  local attribute [instance] premetric.dist_setoid
id                              └───────────────────┘
src                             └───────────────────┘
typ                             └───────────────────┘
doc                             └───────────────────┘
340  
341  def glue_premetric (hΦ : isometry Φ) (hΨ : isometry Ψ) : premetric_space (α ⊕ β) :=
id                            └──────┘         └──────┘     └─────────────┘    
src                           └──────┘          └──────┘      └─────────────┘    
typ                           └──────┘         └──────┘     └─────────────┘    
doc                           └──────┘          └──────┘
342  { dist          := glue_dist Φ Ψ 0,
id                      └───────┘  
src                     └───────┘
typ                     └───────┘  
doc                     └───────┘
343    dist_self     := glue_dist_self Φ Ψ 0,
id                      └────────────┘  
src                     └────────────┘
typ                     └────────────┘  
344    dist_comm     := glue_dist_comm Φ Ψ 0,
id                      └────────────┘  
src                     └────────────┘
typ                     └────────────┘  
345    dist_triangle := glue_dist_triangle Φ Ψ 0 $ λp q, by rw [hΦ.dist_eq, hΨ.dist_eq]; simp }
id                      └────────────────┘         
src                     └────────────────┘                  └──┘          └┘            └───┘
typ                     └────────────────┘              └──┘└────────┘└┘└────────┘  └───┘
doc                                                         └──┘          └┘            └───┘
txt                                                         └──┘          └┘            └───┘
par                                                         └──┘          └┘            └───┘
pid                                                           └┘          └┘                
st                                                         └─────────────┘└──────────┘└─────┘
346  
347  def glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) : Type* :=
id                        └──────┘         └──────┘ 
src                       └──────┘          └──────┘
typ                       └──────┘         └──────┘ 
doc                       └──────┘          └──────┘
348  @metric_quot _ (glue_premetric hΦ hΨ)
id    └─────────┘    └────────────┘ └┘ └┘
src   └─────────┘    └────────────┘
typ   └─────────┘    └────────────┘ └┘ └┘
doc   └─────────┘
349  
350  instance metric_space_glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) :
id                                          └──────┘         └──────┘ 
src                                         └──────┘          └──────┘
typ                                         └──────┘         └──────┘ 
doc                                         └──────┘          └──────┘
351    metric_space (glue_space hΦ hΨ) :=
id     └──────────┘  └────────┘ └┘ └┘
src    └──────────┘  └────────┘
typ    └──────────┘  └────────┘ └┘ └┘
doc    └──────────┘
352  @premetric.metric_space_quot _ (glue_premetric hΦ hΨ)
id    └─────────────────────────┘    └────────────┘ └┘ └┘
src   └─────────────────────────┘    └────────────┘
typ   └─────────────────────────┘    └────────────┘ └┘ └┘
353  
354  def to_glue_l (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : α) : glue_space hΦ hΨ :=
id                       └──────┘         └──────┘            └────────┘ └┘ └┘
src                      └──────┘          └──────┘              └────────┘
typ                      └──────┘         └──────┘            └────────┘ └┘ └┘
doc                      └──────┘          └──────┘
355  by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inl x⟧
id             └─────────────┘         └────────────┘ └┘ └┘        └─┘ 
src     └─────┘└─────────────┘   └───┘└────────────┘      └────┘└─┘ 
typ     └─────┘└─────────────┘ └───┘└────────────┘└┘└┘  └────┘└─┘
doc     └─────┘                   └───┘                    └────┘      
txt     └─────┘                   └───┘                    └────┘      
par     └─────┘                   └───┘                    └────┘      
pid         └┘                   └──┘                               
st     └──────────────────────────────────────────────────────────────────────
356  
src  
typ  
doc  
txt  
par  
pid  
st   
357  def to_glue_r (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : β) : glue_space hΦ hΨ :=
id                       └──────┘         └──────┘            └────────┘ └┘ └┘
src                      └──────┘          └──────┘              └────────┘
typ                      └──────┘         └──────┘            └────────┘ └┘ └┘
doc                      └──────┘          └──────┘
358  by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inr y⟧
id             └─────────────┘         └────────────┘ └┘ └┘        └─┘ 
src     └─────┘└─────────────┘   └───┘└────────────┘      └────┘└─┘ 
typ     └─────┘└─────────────┘ └───┘└────────────┘└┘└┘  └────┘└─┘
doc     └─────┘                   └───┘                    └────┘      
txt     └─────┘                   └───┘                    └────┘      
par     └─────┘                   └───┘                    └────┘      
pid         └┘                   └──┘                               
st     └──────────────────────────────────────────────────────────────────────
359  
src  
typ  
doc  
txt  
par  
pid  
st   
360  instance inhabited_left (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited α] :
id                                 └──────┘         └──────┘    └───────┘ 
src                                └──────┘          └──────┘     └───────┘
typ                                └──────┘         └──────┘    └───────┘ 
doc                                └──────┘          └──────┘
361    inhabited (glue_space hΦ hΨ) :=
id     └───────┘  └────────┘ └┘ └┘
src    └───────┘  └────────┘
typ    └───────┘  └────────┘ └┘ └┘
362  ⟨to_glue_l _ _ (default _)⟩
id    └───────┘      └─────┘
src   └───────┘      └─────┘
typ   └───────┘      └─────┘
363  
364  instance inhabited_right (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited β] :
id                                  └──────┘         └──────┘    └───────┘ 
src                                 └──────┘          └──────┘     └───────┘
typ                                 └──────┘         └──────┘    └───────┘ 
doc                                 └──────┘          └──────┘
365    inhabited (glue_space hΦ hΨ) :=
id     └───────┘  └────────┘ └┘ └┘
src    └───────┘  └────────┘
typ    └───────┘  └────────┘ └┘ └┘
366  ⟨to_glue_r _ _ (default _)⟩
id    └───────┘      └─────┘
src   └───────┘      └─────┘
typ   └───────┘      └─────┘
367  
368  lemma to_glue_commute (hΦ : isometry Φ) (hΨ : isometry Ψ) :
id                               └──────┘         └──────┘ 
src                              └──────┘          └──────┘
typ                              └──────┘         └──────┘ 
doc                              └──────┘          └──────┘
369    (to_glue_l hΦ hΨ) ∘ Φ = (to_glue_r hΦ hΨ) ∘ Ψ :=
id      └───────┘ └┘ └┘      └───────┘ └┘ └┘   
src     └───────┘             └───────┘        
typ     └───────┘ └┘ └┘      └───────┘ └┘ └┘   
370  begin
st   └─────
371    letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ,
id            └─────────────┘         └────────────┘ └┘ └┘
src    └─────┘└─────────────┘   └───┘└────────────┘  
typ    └─────┘└─────────────┘ └───┘└────────────┘└┘└┘
doc    └─────┘                   └───┘                
txt    └─────┘                   └───┘                
par    └─────┘                   └───┘                
pid        └┘                   └──┘                
st   ───────────────────────────────────────────────────────┘└─
372    funext,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
373    simp only [comp, to_glue_l, to_glue_r, quotient.eq],
id                └──┘  └───────┘  └───────┘  └─────────┘
src    └─────────┘└──┘└┘└───────┘└┘└───────┘└┘└─────────┘
typ    └─────────┘└──┘└┘└───────┘└┘└───────┘└┘└─────────┘
doc    └─────────┘    └┘         └┘         └┘           
txt    └─────────┘    └┘         └┘         └┘           
par    └─────────┘    └┘         └┘         └┘           
pid        └──┘└┘    └┘         └┘         └┘           
st   ────────────────────────────────────────────────────┘└─
374    exact glue_dist_glued_points Φ Ψ 0 x
id           └────────────────────┘     
src    └────┘└────────────────────┘  └─┘ 
typ    └────┘└────────────────────┘└─┘
doc    └────┘                        └─┘ 
txt    └────┘                        └─┘ 
par    └────┘                        └─┘ 
pid                                 └─┘ 
st   ──────────────────────────────────────┘
375  end
st   └─┘
376  
377  lemma to_glue_l_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_l hΦ hΨ) :=
id                                  └──────┘         └──────┘     └──────┘  └───────┘ └┘ └┘
src                                 └──────┘          └──────┘      └──────┘  └───────┘
typ                                 └──────┘         └──────┘     └──────┘  └───────┘ └┘ └┘
doc                                 └──────┘          └──────┘      └──────┘
378  isometry_emetric_iff_metric.2 $ λ_ _, rfl
id   └─────────────────────────┘        └─┘
src  └─────────────────────────┘          └─┘
typ  └─────────────────────────┘        └─┘
doc  └─────────────────────────┘
379  
380  lemma to_glue_r_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_r hΦ hΨ) :=
id                                  └──────┘         └──────┘     └──────┘  └───────┘ └┘ └┘
src                                 └──────┘          └──────┘      └──────┘  └───────┘
typ                                 └──────┘         └──────┘     └──────┘  └───────┘ └┘ └┘
doc                                 └──────┘          └──────┘      └──────┘
381  isometry_emetric_iff_metric.2 $ λ_ _, rfl
id   └─────────────────────────┘        └─┘
src  └─────────────────────────┘          └─┘
typ  └─────────────────────────┘        └─┘
doc  └─────────────────────────┘
382  
383  end gluing --section
384  
385  section inductive_limit
386  /- In this section, we define the inductive limit of
387       f 0        f 1        f 2        f 3
388  X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...
389  where the X n are metric spaces and f n isometric embeddings. We do it by defining a premetric
390  space structure on Σn, X n, where the predistance dist x y is obtained by pushing x and y in a
391  common X k using composition by the f n, and taking the distance there. This does not depend on
392  the choice of k as the f n are isometries. The metric space associated to this premetric space
393  is the desired inductive limit.-/
394  open nat
395  
396  variables {X : ℕ → Type u} [∀n, metric_space (X n)] {f : Πn, X n → X (n+1)}
id                                 └──────────┘                      
src                                 └──────────┘                           
typ                                └──────────┘                      
doc                                  └──────────┘
397  
398  /-- Predistance on the disjoint union Σn, X n. -/
399  def inductive_limit_dist (f : Πn, X n → X (n+1)) (x y : Σn, X n) : ℝ :=
id                                                           
src                                                                  
typ                                                          
400  dist (le_rec_on (le_max_left  x.1 y.1) f x.2 : X (max x.1 y.1))
id   └──┘  └───────┘  └─────────┘              └─┘   
src  └──┘  └───────┘  └─────────┘                   └─┘     
typ  └──┘  └───────┘  └─────────┘              └─┘   
doc        └───────┘
401       (le_rec_on (le_max_right x.1 y.1) f y.2 : X (max x.1 y.1))
id         └───────┘  └──────────┘             └─┘   
src        └───────┘  └──────────┘                  └─┘     
typ        └───────┘  └──────────┘             └─┘   
doc        └───────┘
402  
403  /-- The predistance on the disjoint union Σn, X n can be computed in any X k for large enough k.-/
404  lemma inductive_limit_dist_eq_dist (I : ∀n, isometry (f n))
id                                              └──────┘   
src                                              └──────┘
typ                                             └──────┘   
doc                                              └──────┘
405    (x y : Σn, X n) (m : ℕ) : ∀hx : x.1 ≤ m, ∀hy : y.1 ≤ m,
id                                             
src                                                 
typ                                            
406    inductive_limit_dist f x y = dist (le_rec_on hx f x.2 : X m) (le_rec_on hy f y.2 : X m) :=
id     └──────────────────┘     └──┘  └───────┘ └┘          └───────┘ └┘       
src    └──────────────────┘        └──┘  └───────┘                 └───────┘       
typ    └──────────────────┘     └──┘  └───────┘ └┘          └───────┘ └┘       
doc    └──────────────────┘               └───────┘                  └───────┘
407  begin
st   └─────
408    induction m with m hm,
id               
src    └────────┘ └────────┘
typ    └────────┘└────────┘
doc    └────────┘ └────────┘
txt    └────────┘ └────────┘
par    └────────┘ └────────┘
pid              └───────┘
st   ──────────────────────┘└─
409    { assume hx hy,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───┘└──────────┘└─
410      have A : max x.1 y.1 = 0, { rw [le_zero_iff_eq.1 hx, le_zero_iff_eq.1 hy], simp },
id                └─┘                 └────────────┘   └┘  └────────────┘   └┘
src      └───────┘└─┘ └─┘ └─┘└┘    └──┘└────────────┘└─┘  └┘└────────────┘└─┘    └───┘
typ      └───────┘└─┘└─┘└─┘└┘    └──┘└────────────┘└─┘└┘└┘└────────────┘└─┘└┘  └───┘
doc      └───────┘    └─┘ └─┘ └┘    └──┘              └─┘  └┘              └─┘    └───┘
txt      └───────┘    └─┘ └─┘ └┘    └──┘              └─┘  └┘              └─┘    └───┘
par      └───────┘    └─┘ └─┘ └┘    └──┘              └─┘  └┘              └─┘    └───┘
pid      └────┘└─┘    └─┘ └─┘       └┘              └─┘  └┘              └─┘        
st   ───────────────────────────┘└──┘└─────────────────────┘└───────────────────┘└──────┘└┘
411      unfold inductive_limit_dist,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid            └───────────────────┘
st   ──────────────────────────────┘└─
412      congr; simp only [A] },
id                         
src      └───┘  └─────────┘ └┘
typ      └───┘  └─────────┘└┘
doc             └─────────┘ └┘
txt      └───┘  └─────────┘ └┘
par      └───┘  └─────────┘ └┘
pid                 └──┘└┘ 
st   ────────────────────────┘└┘
413    { assume hx hy,
src      └──────────┘
typ      └──────────┘
doc      └──────────┘
txt      └──────────┘
par      └──────────┘
pid      └──────────┘
st   ───────────────┘└─
414      by_cases h : max x.1 y.1 = m.succ,
id                    └─┘         └────┘
src      └───────┘ └─┘└─┘ └─┘ └─┘ └────┘
typ      └───────┘ └─┘└─┘└─┘└─┘ └────┘
doc      └───────┘ └─┘    └─┘ └─┘ 
txt      └───────┘ └─┘    └─┘ └─┘ 
par      └───────┘ └─┘    └─┘ └─┘ 
pid               └─┘    └─┘ └─┘ 
st   ────────────────────────────────────┘└─
415      { unfold inductive_limit_dist,
src        └─────────────────────────┘
typ        └─────────────────────────┘
doc        └─────────────────────────┘
txt        └─────────────────────────┘
par        └─────────────────────────┘
pid              └───────────────────┘
st   ─────┘└─────────────────────────┘└─
416        congr; simp only [h] },
id                           
src        └───┘  └─────────┘ └┘
typ        └───┘  └─────────┘└┘
doc               └─────────┘ └┘
txt        └───┘  └─────────┘ └┘
par        └───┘  └─────────┘ └┘
pid                   └──┘└┘ 
st   ──────────────────────────┘└┘
417      { have : max x.1 y.1 ≤ succ m := by simp [hx, hy],
id                └─┘        └──┘              └┘  └┘
src        └─────┘└─┘ └─┘ └─┘└──┘ └──┘  └────┘  └┘  
typ        └─────┘└─┘└─┘└─┘└──┘└──┘  └────┘└┘└┘└┘
doc        └─────┘    └─┘ └─┘      └──┘  └────┘  └┘  
txt        └─────┘    └─┘ └─┘      └──┘  └────┘  └┘  
par        └─────┘    └─┘ └─┘      └──┘  └────┘  └┘  
pid        └───┘└┘    └─┘ └─┘      └──┘  └─────┘  └┘  
st   ──────────────────────────────────────┘└────────────┘└─
418        have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this,
id                └─┘                               └────────┘ └──┘
src        └─────┘└─┘ └─┘ └─┘  └──┘  └─────┘ └──────┘└────────┘
typ        └─────┘└─┘└─┘└─┘ └──┘  └─────┘└──────┘└────────┘└──┘
doc        └─────┘    └─┘ └─┘  └──┘  └─────┘ └──────┘          
txt        └─────┘    └─┘ └─┘  └──┘  └─────┘ └──────┘          
par        └─────┘    └─┘ └─┘  └──┘  └─────┘ └──────┘          
pid        └───┘└┘    └─┘ └─┘  └──┘  └──────┘ └──────┘          
st   ─────────────────────────────────┘└──────────────────────────────┘└─
419        have xm : x.1 ≤ m := le_trans (le_max_left _ _) this,
id                            └──────┘  └─────────┘      └──┘
src        └────────┘ └─┘  └──┘└──────┘ └─────────┘└────┘
typ        └────────┘└─┘ └──┘└──────┘ └─────────┘└────┘└──┘
doc        └────────┘ └─┘  └──┘                    └────┘
txt        └────────┘ └─┘  └──┘                    └────┘
par        └────────┘ └─┘  └──┘                    └────┘
pid        └─────┘└─┘ └─┘  └──┘                    └────┘
st   ─────────────────────────────────────────────────────────┘└─
420        have ym : y.1 ≤ m := le_trans (le_max_right _ _) this,
id                            └──────┘  └──────────┘      └──┘
src        └────────┘ └─┘  └──┘└──────┘ └──────────┘└────┘
typ        └────────┘└─┘ └──┘└──────┘ └──────────┘└────┘└──┘
doc        └────────┘ └─┘  └──┘                     └────┘
txt        └────────┘ └─┘  └──┘                     └────┘
par        └────────┘ └─┘  └──┘                     └────┘
pid        └─────┘└─┘ └─┘  └──┘                     └────┘
st   ──────────────────────────────────────────────────────────┘└─
421        rw [le_rec_on_succ xm, le_rec_on_succ ym, (I m).dist_eq],
id             └────────────┘ └┘  └────────────┘ └┘    
src        └──┘└────────────┘  └┘└────────────┘  └┘   └────────┘
typ        └──┘└────────────┘└┘└┘└────────────┘└┘└┘ └────────┘
doc        └──┘                └┘                └┘   └────────┘
txt        └──┘                └┘                └┘   └────────┘
par        └──┘                └┘                └┘   └────────┘
pid          └┘                └┘                └┘   └────────┘
st   ──────────────────────────┘└─────────────────┘└────────────┘└───
422        exact hm xm ym }}
id               └┘ └┘ └┘
src        └────┘      
typ        └────┘└┘└┘└┘
doc        └────┘      
txt        └────┘      
par        └────┘      
pid                   
st   ────────────────────┘└──
423  end
st   ──┘
424  
425  /-- Premetric space structure on Σn, X n.-/
426  def inductive_premetric (I : ∀n, isometry (f n)) :
id                                   └──────┘   
src                                   └──────┘
typ                                  └──────┘   
doc                                   └──────┘
427    premetric_space (Σn, X n) :=
id     └─────────────┘    
src    └─────────────┘   
typ    └─────────────┘    
428  { dist          := inductive_limit_dist f,
id                      └──────────────────┘ 
src                     └──────────────────┘
typ                     └──────────────────┘ 
doc                     └──────────────────┘
429    dist_self     := λx, by simp [dist, inductive_limit_dist],
id                                        └──────────────────┘
src                            └────┘    └┘└──────────────────┘
typ                           └────┘    └┘└──────────────────┘
doc                            └────┘    └┘└──────────────────┘
txt                            └────┘    └┘                    
par                            └────┘    └┘                    
pid                                    └┘                    
st                            └────────────────────────────────┘
430    dist_comm     := λx y, begin
id                        
typ                       
st                            └─────
431      let m := max x.1 y.1,
id                └─┘    
src      └───────┘└─┘ └─┘ └┘
typ      └───────┘└─┘└─┘└┘
doc      └───────┘    └─┘ └┘
txt      └───────┘    └─┘ └┘
par      └───────┘    └─┘ └┘
pid      └───┘└─┘    └─┘ └┘
st   ───────────────────────┘└─
432      have hx : x.1 ≤ m := le_max_left _ _,
id                         └─────────┘
src      └────────┘ └─┘ └──┘└─────────┘└──┘
typ      └────────┘└─┘└──┘└─────────┘└──┘
doc      └────────┘ └─┘  └──┘           └──┘
txt      └────────┘ └─┘  └──┘           └──┘
par      └────────┘ └─┘  └──┘           └──┘
pid      └─────┘└─┘ └─┘  └──┘           └──┘
st   ───────────────────────────────────────┘└─
433      have hy : y.1 ≤ m := le_max_right _ _,
id                          └──────────┘
src      └────────┘ └─┘  └──┘└──────────┘└──┘
typ      └────────┘└─┘ └──┘└──────────┘└──┘
doc      └────────┘ └─┘  └──┘            └──┘
txt      └────────┘ └─┘  └──┘            └──┘
par      └────────┘ └─┘  └──┘            └──┘
pid      └─────┘└─┘ └─┘  └──┘            └──┘
st   ────────────────────────────────────────┘└─
434      unfold dist,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
435      rw [inductive_limit_dist_eq_dist I x y m hx hy, inductive_limit_dist_eq_dist I y x m hy hx,
id           └──────────────────────────┘     └┘ └┘  └──────────────────────────┘     └┘ └┘
src      └──┘└──────────────────────────┘        └┘└──────────────────────────┘        └─
typ      └──┘└──────────────────────────┘└┘└┘└┘└──────────────────────────┘└┘└┘└─
doc      └──┘└──────────────────────────┘        └┘└──────────────────────────┘        └─
txt      └──┘                                    └┘                                    └─
par      └──┘                                    └┘                                    └─
pid        └┘                                    └┘                                    └─
st   ─────────────────────────────────────────────────┘└──────────────────────────────────────────┘└─
436          dist_comm]
id           └───────┘
src  ───────┘└───────┘└─
typ  ───────┘└───────┘└─
doc  ───────┘         └─
txt  ───────┘         └─
par  ───────┘         └─
pid  ───────┘         
st   ────────────────┘
437    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
438    dist_triangle := λx y z, begin
id                         
typ                        
st                              └─────
439      let m := max (max x.1 y.1) z.1,
id                     └─┘        
src      └───────┘    └─┘ └─┘ └──┘ └┘
typ      └───────┘    └─┘└─┘└──┘└┘
doc      └───────┘        └─┘ └──┘ └┘
txt      └───────┘        └─┘ └──┘ └┘
par      └───────┘        └─┘ └──┘ └┘
pid      └───┘└─┘        └─┘ └──┘ └┘
st   ─────────────────────────────────┘└─
440      have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _),
id                          └──────┘                    └─────────┘
src      └────────┘ └─┘  └──┘└──────┘            └────┘ └─────────┘└───┘
typ      └────────┘└─┘ └──┘└──────┘            └────┘ └─────────┘└───┘
doc      └────────┘ └─┘  └──┘                    └────┘            └───┘
txt      └────────┘ └─┘  └──┘                    └────┘            └───┘
par      └────────┘ └─┘  └──┘                    └────┘            └───┘
pid      └─────┘└─┘ └─┘  └──┘                    └────┘            └───┘
st   ────────────────────────────────────────────────────────────────────┘└─
441      have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _),
id                          └──────┘  └──────────┘       └─────────┘
src      └────────┘ └─┘  └──┘└──────┘ └──────────┘└────┘ └─────────┘└───┘
typ      └────────┘└─┘ └──┘└──────┘ └──────────┘└────┘ └─────────┘└───┘
doc      └────────┘ └─┘  └──┘                     └────┘            └───┘
txt      └────────┘ └─┘  └──┘                     └────┘            └───┘
par      └────────┘ └─┘  └──┘                     └────┘            └───┘
pid      └─────┘└─┘ └─┘  └──┘                     └────┘            └───┘
st   ─────────────────────────────────────────────────────────────────────┘└─
442      have hz : z.1 ≤ m := le_max_right _ _,
id                          └──────────┘
src      └────────┘ └─┘  └──┘└──────────┘└──┘
typ      └────────┘└─┘ └──┘└──────────┘└──┘
doc      └────────┘ └─┘  └──┘            └──┘
txt      └────────┘ └─┘  └──┘            └──┘
par      └────────┘ └─┘  └──┘            └──┘
pid      └─────┘└─┘ └─┘  └──┘            └──┘
st   ────────────────────────────────────────┘└─
443      calc inductive_limit_dist f x z
id       └──┘
src      └──┘
typ      └──┘
doc      └──┘
st   ────────────────────────────────────
444        = dist (le_rec_on hx f x.2 : X m) (le_rec_on hz f z.2 : X m) :
id           └──┘                             └───────┘           
src          └──┘                             └───────┘
typ          └──┘                             └───────┘           
doc                                           └───────┘
st   ─────────────────────────────────────────────────────────────────────
445          inductive_limit_dist_eq_dist I x z m hx hz
id           └──────────────────────────┘     └┘ └┘
src          └──────────────────────────┘
typ          └──────────────────────────┘     └┘ └┘
doc          └──────────────────────────┘
st   ───────────────────────────────────────────────────
446        ... ≤ dist (le_rec_on hx f x.2 : X m) (le_rec_on hy f y.2 : X m)
id                                                               
src                                                              
typ                                                              
st   ───────────────────────────────────────────────────────────────────────
447            + dist (le_rec_on hy f y.2 : X m) (le_rec_on hz f z.2 : X m) :
id                              └┘                               
src                                                              
typ                             └┘                               
st   ─────────────────────────────────────────────────────────────────────────
448          dist_triangle _ _ _
id           └───────────┘
src          └───────────┘
typ          └───────────┘
st   ────────────────────────────
449        ... = inductive_limit_dist f x y + inductive_limit_dist f y z :
id                                            └──────────────────┘   
src                                           └──────────────────┘
typ                                           └──────────────────┘   
doc                                           └──────────────────┘
st   ──────────────────────────────────────────────────────────────────────
450           by rw [inductive_limit_dist_eq_dist I x y m hx hy,
id                   └──────────────────────────┘     └┘ └┘
src              └──┘└──────────────────────────┘        └─
typ              └──┘└──────────────────────────┘└┘└┘└─
doc              └──┘└──────────────────────────┘        └─
txt              └──┘                                    └─
par              └──┘                                    └─
pid                └┘                                    └─
st   ──────────┘└─────────────────────────────────────────────┘└─
451                  inductive_limit_dist_eq_dist I y z m hy hz]
id                   └──────────────────────────┘     └┘ └┘
src  ───────────────┘└──────────────────────────┘        └─
typ  ───────────────┘└──────────────────────────┘└┘└┘└─
doc  ───────────────┘└──────────────────────────┘        └─
txt  ───────────────┘                                    └─
par  ───────────────┘                                    └─
pid  ───────────────┘                                    
st   ─────────────────────────────────────────────────────────┘
452    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
453  
454  local attribute [instance] inductive_premetric premetric.dist_setoid
id                              └─────────────────┘ └───────────────────┘
src                             └─────────────────┘ └───────────────────┘
typ                             └─────────────────┘ └───────────────────┘
doc                             └─────────────────┘ └───────────────────┘
455  
456  /-- The type giving the inductive limit in a metric space context. -/
457  def inductive_limit (I : ∀n, isometry (f n)) : Type* :=
id                               └──────┘   
src                               └──────┘
typ                              └──────┘   
doc                               └──────┘
458  @metric_quot _ (inductive_premetric I)
id    └─────────┘    └─────────────────┘ 
src   └─────────┘    └─────────────────┘
typ   └─────────┘    └─────────────────┘ 
doc   └─────────┘    └─────────────────┘
459  
460  /-- Metric space structure on the inductive limit. -/
461  instance metric_space_inductive_limit (I : ∀n, isometry (f n)) :
id                                                 └──────┘   
src                                                 └──────┘
typ                                                └──────┘   
doc                                                 └──────┘
462    metric_space (inductive_limit I) :=
id     └──────────┘  └─────────────┘ 
src    └──────────┘  └─────────────┘
typ    └──────────┘  └─────────────┘ 
doc    └──────────┘  └─────────────┘
463  @premetric.metric_space_quot _ (inductive_premetric I)
id    └─────────────────────────┘    └─────────────────┘ 
src   └─────────────────────────┘    └─────────────────┘
typ   └─────────────────────────┘    └─────────────────┘ 
doc                                  └─────────────────┘
464  
465  /-- Mapping each `X n` to the inductive limit. -/
466  def to_inductive_limit (I : ∀n, isometry (f n)) (n : ℕ) (x : X n) : metric.inductive_limit I :=
id                                  └──────┘                       └────────────────────┘ 
src                                  └──────┘                           └────────────────────┘
typ                                 └──────┘                       └────────────────────┘ 
doc                                  └──────┘                            └────────────────────┘
467  by letI : premetric_space (Σn, X n) := inductive_premetric I; exact ⟦sigma.mk n x⟧
id             └─────────────┘           └─────────────────┘         └──────┘  
src     └─────┘└─────────────┘   └───┘└─────────────────┘   └────┘└──────┘  
typ     └─────┘└─────────────┘  └───┘└─────────────────┘  └────┘└──────┘
doc     └─────┘                    └───┘└─────────────────┘   └────┘            
txt     └─────┘                    └───┘                      └────┘            
par     └─────┘                    └───┘                      └────┘            
pid         └┘                    └──┘                                       
st     └────────────────────────────────────────────────────────────────────────────────
468  
src  
typ  
doc  
txt  
par  
pid  
st   
469  instance (I : ∀ n, isometry (f n)) [inhabited (X 0)] : inhabited (inductive_limit I) :=
id                     └──────┘       └───────┘         └───────┘  └─────────────┘ 
src                     └──────┘         └───────┘          └───────┘  └─────────────┘
typ                    └──────┘       └───────┘         └───────┘  └─────────────┘ 
doc                     └──────┘                                       └─────────────┘
470  ⟨to_inductive_limit _ 0 (default _)⟩
id    └────────────────┘      └─────┘
src   └────────────────┘      └─────┘
typ   └────────────────┘      └─────┘
doc   └────────────────┘
471  
472  /-- The map `to_inductive_limit n` mapping `X n` to the inductive limit is an isometry. -/
473  lemma to_inductive_limit_isometry (I : ∀n, isometry (f n)) (n : ℕ) :
id                                             └──────┘           
src                                             └──────┘             
typ                                            └──────┘           
doc                                             └──────┘
474    isometry (to_inductive_limit I n) := isometry_emetric_iff_metric.2 $ λx y,
id     └──────┘  └────────────────┘       └─────────────────────────┘      
src    └──────┘  └────────────────┘         └─────────────────────────┘
typ    └──────┘  └────────────────┘       └─────────────────────────┘      
doc    └──────┘  └────────────────┘         └─────────────────────────┘
475  begin
st   └─────
476    change inductive_limit_dist f ⟨n, x⟩ ⟨n, y⟩ = dist x y,
id            └──────────────────┘                └──┘  
src    └─────┘└──────────────────┘   └┘ └┘  └┘ └┘└──┘ 
typ    └─────┘└──────────────────┘  └┘ └┘ └┘ └┘└──┘
doc    └─────┘└──────────────────┘   └┘ └┘  └┘ └┘      
txt    └─────┘                       └┘ └┘  └┘ └┘      
par    └─────┘                       └┘ └┘  └┘ └┘      
pid                                 └┘ └┘  └┘ └┘      
st   ───────────────────────────────────────────────────────┘└─
477    rw [inductive_limit_dist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n),
id         └──────────────────────────┘                             └─────┘ 
src    └──┘└──────────────────────────┘   └┘ └┘  └┘ └┘          └┘ └─────┘ └──
typ    └──┘└──────────────────────────┘  └┘└┘  └┘└┘          └┘ └─────┘└──
doc    └──┘└──────────────────────────┘   └┘ └┘  └┘ └┘          └┘         └──
txt    └──┘                               └┘ └┘  └┘ └┘          └┘         └──
par    └──┘                               └┘ └┘  └┘ └┘          └┘         └──
pid      └┘                               └┘ └┘  └┘ └┘          └┘         └──
st   ───────────────────────────────────────────────────────────────────────────┘└─
478        le_rec_on_self, le_rec_on_self]
id         └────────────┘  └────────────┘
src  ─────┘└────────────┘└┘└────────────┘└┘
typ  ─────┘└────────────┘└┘└────────────┘└┘
doc  ─────┘              └┘              └┘
txt  ─────┘              └┘              └┘
par  ─────┘              └┘              └┘
pid  ─────┘              └┘              
st   ───────────────────┘└──────────────┘
479  end
st   └─┘
480  
481  /-- The maps `to_inductive_limit n` are compatible with the maps `f n`. -/
482  lemma to_inductive_limit_commute (I : ∀n, isometry (f n)) (n : ℕ) :
id                                            └──────┘           
src                                            └──────┘             
typ                                           └──────┘           
doc                                            └──────┘
483    (to_inductive_limit I n.succ) ∘ (f n) = to_inductive_limit I n :=
id      └────────────────┘  └───┘        └────────────────┘  
src     └────────────────┘    └───┘          └────────────────┘
typ     └────────────────┘  └───┘        └────────────────┘  
doc     └────────────────┘                     └────────────────┘
484  begin
st   └─────
485    funext,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
st   ───────┘└─
486    simp only [comp, to_inductive_limit, quotient.eq],
id                └──┘  └────────────────┘  └─────────┘
src    └─────────┘└──┘└┘└────────────────┘└┘└─────────┘
typ    └─────────┘└──┘└┘└────────────────┘└┘└─────────┘
doc    └─────────┘    └┘└────────────────┘└┘           
txt    └─────────┘    └┘                  └┘           
par    └─────────┘    └┘                  └┘           
pid        └──┘└┘    └┘                  └┘           
st   ──────────────────────────────────────────────────┘└─
487    show inductive_limit_dist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0,
id          └──────────────────┘    └────┘             
src    └───┘└──────────────────┘  └────┘└┘   └┘  └┘ └┘└┘
typ    └───┘└──────────────────┘  └────┘└┘  └┘ └┘└┘└┘
doc    └───┘└──────────────────┘        └┘   └┘  └┘ └┘ └┘
txt    └───┘                            └┘   └┘  └┘ └┘ └┘
par    └───┘                            └┘   └┘  └┘ └┘ └┘
pid    └───┘                            └┘   └┘  └┘ └┘ 
st   ───────────────────────────────────────────────────────┘└─
488    { rw [inductive_limit_dist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ,
id           └──────────────────────────┘                       └────┘
src      └──┘└──────────────────────────┘        └┘   └┘  └┘ └┘└────┘└─
typ      └──┘└──────────────────────────┘       └┘  └┘  └┘└┘└────┘└─
doc      └──┘└──────────────────────────┘        └┘   └┘  └┘ └┘      └─
txt      └──┘                                    └┘   └┘  └┘ └┘      └─
par      └──┘                                    └┘   └┘  └┘ └┘      └─
pid        └┘                                    └┘   └┘  └┘ └┘      └─
st   ───────────────────────────────────────────────────────────────────┘└─
489          le_rec_on_self, le_rec_on_succ, le_rec_on_self, dist_self],
id           └────────────┘  └────────────┘  └────────────┘  └───────┘
src  ───────┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘
typ  ───────┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘
doc  ───────┘              └┘              └┘              └┘         
txt  ───────┘              └┘              └┘              └┘         
par  ───────┘              └┘              └┘              └┘         
pid  ───────┘              └┘              └┘              └┘         
st   ─────────────────────┘└──────────────┘└──────────────┘└─────────┘└──
490      exact le_refl _,
id             └─────┘
src      └────┘└─────┘└┘
typ      └────┘└─────┘└┘
doc      └────┘       └┘
txt      └────┘       └┘
par      └────┘       └┘
pid                  └┘
st   ──────────────────┘└─
491      exact le_refl _,
id             └─────┘
src      └────┘└─────┘└┘
typ      └────┘└─────┘└┘
doc      └────┘       └┘
txt      └────┘       └┘
par      └────┘       └┘
pid                  └┘
st   ──────────────────┘└─
492      exact le_succ _ }
id             └─────┘
src      └────┘└─────┘└─┘
typ      └────┘└─────┘└─┘
doc      └────┘       └─┘
txt      └────┘       └─┘
par      └────┘       └─┘
pid                  └┘
st   ───────────────────┘└─
493  end
st   ──┘
494  
495  end inductive_limit --section
496  end metric --namespace